Theorem biadanii 833

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  elab4g  3642  elpwb  4570  ssdifsn  4756  brab2a  5754  elon2  6371  elovmpo  7655  eqop2  8025  iscard  9957  iscard2  9958  elnnnn0  12542  elfzo2  13686  bitsval  16477  1nprm  16732  funcpropd  17954  isfull  17964  isfth  17968  ismgmhm  18749  ismhm  18838  isghm  19281  ghmpropd  19321  isga  19356  oppgcntz  19429  gexdvdsi  19648  isrnghm  20519  isrhm  20557  issdrg  20891  abvpropd  20938  islmhm  21148  dfprm2  21623  prmirred  21624  elocv  21818  isobs  21870  iscn2  23395  iscnp2  23396  islocfin  23674  elflim2  24121  isfcls  24166  isnghm  24880  isnmhm  24903  0plef  25831  elply  26352  dchrelbas4  27407  brslts  27955  nb3grpr  29732  ispligb  30829  isph  31174  abfmpunirn  32997  iscvm  35751  sscoid  36403  bj-pwvrelb  37553  bj-elsnb  37717  bj-ideqb  37823  bj-opelidb1ALT  37830  bj-elid5  37833  eldiophb  43508  eldioph3b  43516  eldioph4b  43558  bropabg  44070  brfvrcld2  44438  islmd  50463  iscmd  50464