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

Theorem biadan2 673
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 664 . 2 (𝜑 ↔ (𝜓𝜑))
3 biadan2.2 . . 3 (𝜓 → (𝜑𝜒))
43pm5.32i 668 . 2 ((𝜓𝜑) ↔ (𝜓𝜒))
52, 4bitri 264 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  elab4g  3338  brab2a  5129  brab2ga  5155  elon2  5693  elovmpt2  6832  eqop2  7154  iscard  8745  iscard2  8746  elnnnn0  11280  elfzo2  12414  bitsval  15070  1nprm  15316  funcpropd  16481  isfull  16491  isfth  16495  ismhm  17258  isghm  17581  ghmpropd  17619  isga  17645  oppgcntz  17715  gexdvdsi  17919  isrhm  18642  abvpropd  18763  islmhm  18946  dfprm2  19761  prmirred  19762  elocv  19931  isobs  19983  iscn2  20952  iscnp2  20953  islocfin  21230  elflim2  21678  isfcls  21723  isnghm  22437  isnmhm  22460  0plef  23345  elply  23855  dchrelbas4  24868  nb3grpr  26171  isph  27523  abfmpunirn  29291  iscvm  30946  sscoid  31659  eldiophb  36797  eldioph3b  36805  eldioph4b  36852  issdrg  37245  brfvrcld2  37462  ismgmhm  41068  isrnghm  41177
  Copyright terms: Public domain W3C validator