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 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  3634  elpwb  4555  ssdifsn  4737  brab2a  5707  elon2  6317  elovmpo  7591  eqop2  7964  iscard  9868  iscard2  9869  elnnnn0  12424  elfzo2  13562  bitsval  16335  1nprm  16590  funcpropd  17809  isfull  17819  isfth  17823  ismgmhm  18604  ismhm  18693  isghm  19127  isghmOLD  19128  ghmpropd  19168  isga  19203  oppgcntz  19276  gexdvdsi  19495  isrnghm  20359  isrhm  20396  issdrg  20703  abvpropd  20750  islmhm  20961  dfprm2  21410  prmirred  21411  elocv  21605  isobs  21657  iscn2  23153  iscnp2  23154  islocfin  23432  elflim2  23879  isfcls  23924  isnghm  24638  isnmhm  24661  0plef  25600  elply  26127  dchrelbas4  27181  brsslt  27725  nb3grpr  29360  ispligb  30457  isph  30802  abfmpunirn  32634  iscvm  35303  sscoid  35955  bj-pwvrelb  36942  bj-elsnb  37105  bj-ideqb  37203  bj-opelidb1ALT  37210  bj-elid5  37213  eldiophb  42860  eldioph3b  42868  eldioph4b  42914  bropabg  43426  brfvrcld2  43795  islmd  49776  iscmd  49777