Theorem biadanii 820

Description: Inference associated with biadani 818. 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 818	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 232	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  elab4g  3671  elpwb  4549  ssdifsn  4720  brab2a  5644  elon2  6202  elovmpo  7390  eqop2  7732  iscard  9404  iscard2  9405  elnnnn0  11941  elfzo2  13042  bitsval  15773  1nprm  16023  funcpropd  17170  isfull  17180  isfth  17184  ismhm  17958  isghm  18358  ghmpropd  18396  isga  18421  oppgcntz  18492  gexdvdsi  18708  isrhm  19473  issdrg  19574  abvpropd  19613  islmhm  19799  dfprm2  20641  prmirred  20642  elocv  20812  isobs  20864  iscn2  21846  iscnp2  21847  islocfin  22125  elflim2  22572  isfcls  22617  isnghm  23332  isnmhm  23355  0plef  24273  elply  24785  dchrelbas4  25819  nb3grpr  27164  ispligb  28254  isph  28599  abfmpunirn  30397  iscvm  32506  brsslt  33254  sscoid  33374  bj-pwvrelb  34217  bj-elsnb  34357  bj-ideqb  34454  bj-opelidb1ALT  34461  bj-elid5  34464  eldiophb  39403  eldioph3b  39411  eldioph4b  39457  brfvrcld2  40086  ismgmhm  44099  isrnghm  44212