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

Theorem biadanii 821
Description: Inference associated with biadani 819. 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 819 . 2 ((𝜓 → (𝜑𝜒)) ↔ (𝜑 ↔ (𝜓𝜒)))
41, 3mpbi 233 1 (𝜑 ↔ (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  elab4g  3657  elpwb  4532  ssdifsn  4705  brab2a  5632  elon2  6190  elovmpo  7381  eqop2  7724  iscard  9397  iscard2  9398  elnnnn0  11935  elfzo2  13043  bitsval  15769  1nprm  16019  funcpropd  17168  isfull  17178  isfth  17182  ismhm  17956  isghm  18356  ghmpropd  18394  isga  18419  oppgcntz  18490  gexdvdsi  18706  isrhm  19471  issdrg  19569  abvpropd  19608  islmhm  19794  dfprm2  20636  prmirred  20637  elocv  20807  isobs  20859  iscn2  21841  iscnp2  21842  islocfin  22120  elflim2  22567  isfcls  22612  isnghm  23327  isnmhm  23350  0plef  24274  elply  24790  dchrelbas4  25825  nb3grpr  27170  ispligb  28258  isph  28603  abfmpunirn  30403  iscvm  32533  brsslt  33281  sscoid  33401  bj-pwvrelb  34252  bj-elsnb  34392  bj-ideqb  34489  bj-opelidb1ALT  34496  bj-elid5  34499  eldiophb  39554  eldioph3b  39562  eldioph4b  39608  brfvrcld2  40249  ismgmhm  44269  isrnghm  44382
  Copyright terms: Public domain W3C validator