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  3637  elpwb  4565  ssdifsn  4751  brab2a  5744  elon2  6373  elovmpo  7666  eqop2  8044  iscard  10056  iscard2  10057  elnnnn0  12649  elfzo2  13796  bitsval  16594  1nprm  16854  funcpropd  18077  isfull  18087  isfth  18091  ismgmhm  18885  ismhm  18980  isghm  19430  ghmpropd  19470  isga  19505  oppgcntz  19578  gexdvdsi  19797  isrnghm  20671  isrhm  20709  issdrg  21045  abvpropd  21092  islmhm  21302  dfprm2  21779  prmirred  21780  elocv  21974  isobs  22026  iscn2  23556  iscnp2  23557  islocfin  23836  elflim2  24283  isfcls  24328  isnghm  25042  isnmhm  25065  0plef  25993  elply  26513  dchrelbas4  27570  brslts  28148  nb3grpr  29963  ispligb  31079  isph  31424  abfmpunirn  33246  iscvm  36024  sscoid  36675  bj-pwvrelb  37810  bj-elsnb  37976  bj-ideqb  38080  bj-opelidb1ALT  38087  bj-elid5  38090  eldiophb  43767  eldioph3b  43775  eldioph4b  43817  bropabg  44324  brfvrcld2  44691  islmd  50772  iscmd  50773