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

Theorem biadan2 677
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 668 . 2 (𝜑 ↔ (𝜓𝜑))
3 biadan2.2 . . 3 (𝜓 → (𝜑𝜒))
43pm5.32i 672 . 2 ((𝜓𝜑) ↔ (𝜓𝜒))
52, 4bitri 264 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383
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 385
This theorem is referenced by:  elab4g  3495  elpwb  4313  ssdifsn  4463  brab2a  5351  elon2  5895  elovmpt2  7044  eqop2  7376  iscard  8991  iscard2  8992  elnnnn0  11528  elfzo2  12667  bitsval  15348  1nprm  15594  funcpropd  16761  isfull  16771  isfth  16775  ismhm  17538  isghm  17861  ghmpropd  17899  isga  17924  oppgcntz  17994  gexdvdsi  18198  isrhm  18923  abvpropd  19044  islmhm  19229  dfprm2  20044  prmirred  20045  elocv  20214  isobs  20266  iscn2  21244  iscnp2  21245  islocfin  21522  elflim2  21969  isfcls  22014  isnghm  22728  isnmhm  22751  0plef  23638  elply  24150  dchrelbas4  25167  nb3grpr  26482  ispligb  27640  isph  27986  abfmpunirn  29761  iscvm  31548  brsslt  32206  sscoid  32326  bj-ismoorec  33366  eldiophb  37822  eldioph3b  37830  eldioph4b  37877  issdrg  38269  brfvrcld2  38486  ismgmhm  42293  isrnghm  42402
  Copyright terms: Public domain W3C validator