Theorem biadanii 831

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

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

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 400

This theorem is referenced by:  elab4g  3642  elpwb  4563  ssdifsn  4748  brab2a  5740  elon2  6357  elovmpo  7641  eqop2  8013  iscard  9933  iscard2  9934  elnnnn0  12524  elfzo2  13667  bitsval  16458  1nprm  16713  funcpropd  17935  isfull  17945  isfth  17949  ismgmhm  18730  ismhm  18819  isghm  19256  ghmpropd  19296  isga  19331  oppgcntz  19404  gexdvdsi  19623  isrnghm  20490  isrhm  20527  issdrg  20837  abvpropd  20884  islmhm  21094  dfprm2  21525  prmirred  21526  elocv  21720  isobs  21772  iscn2  23298  iscnp2  23299  islocfin  23577  elflim2  24024  isfcls  24069  isnghm  24783  isnmhm  24806  0plef  25734  elply  26255  dchrelbas4  27307  brslts  27855  nb3grpr  29583  ispligb  30680  isph  31025  abfmpunirn  32854  iscvm  35609  sscoid  36261  bj-pwvrelb  37383  bj-elsnb  37546  bj-ideqb  37651  bj-opelidb1ALT  37658  bj-elid5  37661  eldiophb  43338  eldioph3b  43346  eldioph4b  43388  bropabg  43900  brfvrcld2  44268  islmd  50286  iscmd  50287