Theorem biadanii 828

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

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

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 398

This theorem is referenced by:  elab4g  3623  elpwb  4540  ssdifsn  4724  brab2a  5714  elon2  6325  elovmpo  7605  eqop2  7978  iscard  9894  iscard2  9895  elnnnn0  12475  elfzo2  13611  bitsval  16388  1nprm  16643  funcpropd  17864  isfull  17874  isfth  17878  ismgmhm  18659  ismhm  18748  isghm  19185  isghmOLD  19186  ghmpropd  19226  isga  19261  oppgcntz  19334  gexdvdsi  19553  isrnghm  20416  isrhm  20453  issdrg  20764  abvpropd  20811  islmhm  21021  dfprm2  21452  prmirred  21453  elocv  21647  isobs  21699  iscn2  23225  iscnp2  23226  islocfin  23504  elflim2  23951  isfcls  23996  isnghm  24710  isnmhm  24733  0plef  25661  elply  26182  dchrelbas4  27228  brslts  27776  nb3grpr  29473  ispligb  30570  isph  30915  abfmpunirn  32748  iscvm  35502  sscoid  36154  bj-pwvrelb  37266  bj-elsnb  37429  bj-ideqb  37534  bj-opelidb1ALT  37541  bj-elid5  37544  eldiophb  43221  eldioph3b  43229  eldioph4b  43271  bropabg  43783  brfvrcld2  44151  islmd  50169  iscmd  50170