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  3651  elpwb  4575  ssdifsn  4760  brab2a  5755  elon2  6372  elovmpo  7656  eqop2  8029  iscard  9961  iscard2  9962  elnnnn0  12547  elfzo2  13690  bitsval  16482  1nprm  16737  funcpropd  17959  isfull  17969  isfth  17973  ismgmhm  18754  ismhm  18843  isghm  19286  ghmpropd  19326  isga  19361  oppgcntz  19434  gexdvdsi  19653  isrnghm  20523  isrhm  20560  issdrg  20869  abvpropd  20916  islmhm  21126  dfprm2  21592  prmirred  21593  elocv  21787  isobs  21839  iscn2  23364  iscnp2  23365  islocfin  23643  elflim2  24090  isfcls  24135  isnghm  24849  isnmhm  24872  0plef  25800  elply  26321  dchrelbas4  27373  brslts  27921  nb3grpr  29673  ispligb  30770  isph  31115  abfmpunirn  32938  iscvm  35650  sscoid  36302  bj-pwvrelb  37422  bj-elsnb  37585  bj-ideqb  37691  bj-opelidb1ALT  37698  bj-elid5  37701  eldiophb  43380  eldioph3b  43388  eldioph4b  43430  bropabg  43942  brfvrcld2  44310  islmd  50328  iscmd  50329