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 229	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  elab4g  3672  elpwb  4609  ssdifsn  4790  brab2a  5767  elon2  6372  elovmpo  7647  eqop2  8014  iscard  9966  iscard2  9967  elnnnn0  12511  elfzo2  13631  bitsval  16361  1nprm  16612  funcpropd  17847  isfull  17857  isfth  17861  ismhm  18669  isghm  19086  ghmpropd  19124  isga  19149  oppgcntz  19225  gexdvdsi  19445  isrhm  20249  issdrg  20396  abvpropd  20442  islmhm  20630  dfprm2  21034  prmirred  21035  elocv  21212  isobs  21266  iscn2  22733  iscnp2  22734  islocfin  23012  elflim2  23459  isfcls  23504  isnghm  24231  isnmhm  24254  0plef  25180  elply  25700  dchrelbas4  26735  brsslt  27276  nb3grpr  28628  ispligb  29717  isph  30062  abfmpunirn  31864  iscvm  34238  sscoid  34873  bj-pwvrelb  35766  bj-elsnb  35930  bj-ideqb  36028  bj-opelidb1ALT  36035  bj-elid5  36038  eldiophb  41480  eldioph3b  41488  eldioph4b  41534  bropabg  42058  brfvrcld2  42428  ismgmhm  46539  isrnghm  46675