Theorem biadanii 822

Description: Inference associated with biadani 820. 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 820	. 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  3640  elpwb  4564  ssdifsn  4746  brab2a  5725  elon2  6336  elovmpo  7613  eqop2  7986  iscard  9899  iscard2  9900  elnnnn0  12456  elfzo2  13590  bitsval  16363  1nprm  16618  funcpropd  17838  isfull  17848  isfth  17852  ismgmhm  18633  ismhm  18722  isghm  19156  isghmOLD  19157  ghmpropd  19197  isga  19232  oppgcntz  19305  gexdvdsi  19524  isrnghm  20389  isrhm  20426  issdrg  20733  abvpropd  20780  islmhm  20991  dfprm2  21440  prmirred  21441  elocv  21635  isobs  21687  iscn2  23194  iscnp2  23195  islocfin  23473  elflim2  23920  isfcls  23965  isnghm  24679  isnmhm  24702  0plef  25641  elply  26168  dchrelbas4  27222  brslts  27770  nb3grpr  29467  ispligb  30565  isph  30910  abfmpunirn  32742  iscvm  35475  sscoid  36127  bj-pwvrelb  37146  bj-elsnb  37309  bj-ideqb  37414  bj-opelidb1ALT  37421  bj-elid5  37424  eldiophb  43114  eldioph3b  43122  eldioph4b  43168  bropabg  43680  brfvrcld2  44048  islmd  50024  iscmd  50025