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  3662  elpwb  4583  ssdifsn  4764  brab2a  5748  elon2  6363  elovmpo  7650  eqop2  8029  iscard  9987  iscard2  9988  elnnnn0  12542  elfzo2  13677  bitsval  16441  1nprm  16696  funcpropd  17913  isfull  17923  isfth  17927  ismgmhm  18672  ismhm  18761  isghm  19196  isghmOLD  19197  ghmpropd  19237  isga  19272  oppgcntz  19345  gexdvdsi  19562  isrnghm  20399  isrhm  20436  issdrg  20746  abvpropd  20793  islmhm  20983  dfprm2  21432  prmirred  21433  elocv  21626  isobs  21678  iscn2  23174  iscnp2  23175  islocfin  23453  elflim2  23900  isfcls  23945  isnghm  24660  isnmhm  24683  0plef  25623  elply  26150  dchrelbas4  27204  brsslt  27747  nb3grpr  29307  ispligb  30404  isph  30749  abfmpunirn  32576  iscvm  35227  sscoid  35877  bj-pwvrelb  36862  bj-elsnb  37025  bj-ideqb  37123  bj-opelidb1ALT  37130  bj-elid5  37133  eldiophb  42727  eldioph3b  42735  eldioph4b  42781  bropabg  43294  brfvrcld2  43663  islmd  49483  iscmd  49484