Theorem biadanii 820

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

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

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 399

This theorem is referenced by:  elab4g  3670  elpwb  4551  ssdifsn  4713  brab2a  5638  elon2  6196  elovmpo  7384  eqop2  7726  iscard  9398  iscard2  9399  elnnnn0  11934  elfzo2  13035  bitsval  15767  1nprm  16017  funcpropd  17164  isfull  17174  isfth  17178  ismhm  17952  isghm  18352  ghmpropd  18390  isga  18415  oppgcntz  18486  gexdvdsi  18702  isrhm  19467  issdrg  19568  abvpropd  19607  islmhm  19793  dfprm2  20635  prmirred  20636  elocv  20806  isobs  20858  iscn2  21840  iscnp2  21841  islocfin  22119  elflim2  22566  isfcls  22611  isnghm  23326  isnmhm  23349  0plef  24267  elply  24779  dchrelbas4  25813  nb3grpr  27158  ispligb  28248  isph  28593  abfmpunirn  30391  iscvm  32501  brsslt  33249  sscoid  33369  bj-pwvrelb  34209  bj-elsnb  34348  bj-ideqb  34445  bj-opelidb1ALT  34452  bj-elid5  34455  eldiophb  39347  eldioph3b  39355  eldioph4b  39401  brfvrcld2  40030  ismgmhm  44044  isrnghm  44157