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

Step	Hyp	Ref	Expression
1		biadanii.2	. 2 ⊢ (𝜓 → (𝜑 ↔ 𝜒))
2		biadani.1	. . 3 ⊢ (𝜑 → 𝜓)
3	2	biadani 820	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 230	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

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