Theorem biadanii 834

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  elab4g  3636  elpwb  4564  ssdifsn  4750  brab2a  5743  cnveq0b  6191  elon2  6373  elovmpo  7666  eqop2  8044  iscard  10057  iscard2  10058  elnnnn0  12650  elfzo2  13797  bitsval  16595  1nprm  16855  funcpropd  18078  isfull  18088  isfth  18092  ismgmhm  18886  ismhm  18981  isghm  19431  ghmpropd  19471  isga  19506  oppgcntz  19579  gexdvdsi  19798  isrnghm  20672  isrhm  20710  issdrg  21046  abvpropd  21093  islmhm  21303  dfprm2  21780  prmirred  21781  elocv  21975  isobs  22027  iscn2  23557  iscnp2  23558  islocfin  23837  elflim2  24284  isfcls  24329  isnghm  25043  isnmhm  25066  0plef  25994  elply  26514  dchrelbas4  27571  brslts  28149  nb3grpr  29964  ispligb  31080  isph  31425  abfmpunirn  33289  iscvm  36093  sscoid  36750  bj-pwvrelb  37885  bj-elsnb  38051  bj-ideqb  38156  bj-opelidb1ALT  38163  bj-elid5  38166  eldiophb  43844  eldioph3b  43852  eldioph4b  43894  bropabg  44401  brfvrcld2  44768  islmd  50849  iscmd  50850