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

Theorem biadanii 822
Description: Inference associated with biadani 820. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)
Hypotheses
Ref Expression
biadani.1 (𝜑𝜓)
biadanii.2 (𝜓 → (𝜑𝜒))
Assertion
Ref Expression
biadanii (𝜑 ↔ (𝜓𝜒))

Proof of Theorem biadanii
StepHypRef Expression
1 biadanii.2 . 2 (𝜓 → (𝜑𝜒))
2 biadani.1 . . 3 (𝜑𝜓)
32biadani 820 . 2 ((𝜓 → (𝜑𝜒)) ↔ (𝜑 ↔ (𝜓𝜒)))
41, 3mpbi 230 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  elab4g  3683  elpwb  4608  ssdifsn  4788  brab2a  5779  elon2  6395  elovmpo  7678  eqop2  8057  iscard  10015  iscard2  10016  elnnnn0  12569  elfzo2  13702  bitsval  16461  1nprm  16716  funcpropd  17947  isfull  17957  isfth  17961  ismgmhm  18709  ismhm  18798  isghm  19233  isghmOLD  19234  ghmpropd  19274  isga  19309  oppgcntz  19383  gexdvdsi  19601  isrnghm  20441  isrhm  20478  issdrg  20789  abvpropd  20836  islmhm  21026  dfprm2  21484  prmirred  21485  elocv  21686  isobs  21740  iscn2  23246  iscnp2  23247  islocfin  23525  elflim2  23972  isfcls  24017  isnghm  24744  isnmhm  24767  0plef  25707  elply  26234  dchrelbas4  27287  brsslt  27830  nb3grpr  29399  ispligb  30496  isph  30841  abfmpunirn  32662  iscvm  35264  sscoid  35914  bj-pwvrelb  36899  bj-elsnb  37062  bj-ideqb  37160  bj-opelidb1ALT  37167  bj-elid5  37170  eldiophb  42768  eldioph3b  42776  eldioph4b  42822  bropabg  43336  brfvrcld2  43705
  Copyright terms: Public domain W3C validator