MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biadan2 Structured version   Visualization version   GIF version

Theorem biadan2 820
Description: Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
Hypotheses
Ref Expression
biadan2.1 (𝜑𝜓)
biadan2.2 (𝜓 → (𝜑𝜒))
Assertion
Ref Expression
biadan2 (𝜑 ↔ (𝜓𝜒))

Proof of Theorem biadan2
StepHypRef Expression
1 biadan2.1 . . 3 (𝜑𝜓)
21pm4.71ri 550 . 2 (𝜑 ↔ (𝜓𝜑))
3 biadan2.2 . . 3 (𝜓 → (𝜑𝜒))
43pm5.32i 564 . 2 ((𝜓𝜑) ↔ (𝜓𝜒))
52, 4bitri 264 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 383
This theorem is referenced by:  elab4g  3506  elpwb  4308  ssdifsn  4454  brab2a  5334  elon2  5877  elovmpt2  7026  eqop2  7358  iscard  9001  iscard2  9002  elnnnn0  11538  elfzo2  12681  bitsval  15354  1nprm  15599  funcpropd  16767  isfull  16777  isfth  16781  ismhm  17545  isghm  17868  ghmpropd  17906  isga  17931  oppgcntz  18001  gexdvdsi  18205  isrhm  18931  abvpropd  19052  islmhm  19240  dfprm2  20057  prmirred  20058  elocv  20229  isobs  20281  iscn2  21263  iscnp2  21264  islocfin  21541  elflim2  21988  isfcls  22033  isnghm  22747  isnmhm  22770  0plef  23659  elply  24171  dchrelbas4  25189  nb3grpr  26507  ispligb  27671  isph  28017  abfmpunirn  29792  iscvm  31579  brsslt  32237  sscoid  32357  bj-ismoorec  33392  eldiophb  37846  eldioph3b  37854  eldioph4b  37901  issdrg  38293  brfvrcld2  38510  ismgmhm  42311  isrnghm  42420
  Copyright terms: Public domain W3C validator