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

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

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  3619  elpwb  4507  ssdifsn  4681  brab2a  5608  elon2  6170  elovmpo  7370  eqop2  7714  iscard  9388  iscard2  9389  elnnnn0  11928  elfzo2  13036  bitsval  15763  1nprm  16013  funcpropd  17162  isfull  17172  isfth  17176  ismhm  17950  isghm  18350  ghmpropd  18388  isga  18413  oppgcntz  18484  gexdvdsi  18700  isrhm  19469  issdrg  19567  abvpropd  19606  islmhm  19792  dfprm2  20187  prmirred  20188  elocv  20357  isobs  20409  iscn2  21843  iscnp2  21844  islocfin  22122  elflim2  22569  isfcls  22614  isnghm  23329  isnmhm  23352  0plef  24276  elply  24792  dchrelbas4  25827  nb3grpr  27172  ispligb  28260  isph  28605  abfmpunirn  30415  iscvm  32619  brsslt  33367  sscoid  33487  bj-pwvrelb  34338  bj-elsnb  34478  bj-ideqb  34574  bj-opelidb1ALT  34581  bj-elid5  34584  eldiophb  39698  eldioph3b  39706  eldioph4b  39752  brfvrcld2  40393  ismgmhm  44403  isrnghm  44516