Theorem biadanii 822

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  elab4g  3626  elpwb  4549  ssdifsn  4733  brab2a  5724  elon2  6334  elovmpo  7612  eqop2  7985  iscard  9899  iscard2  9900  elnnnn0  12480  elfzo2  13616  bitsval  16393  1nprm  16648  funcpropd  17869  isfull  17879  isfth  17883  ismgmhm  18664  ismhm  18753  isghm  19190  isghmOLD  19191  ghmpropd  19231  isga  19266  oppgcntz  19339  gexdvdsi  19558  isrnghm  20421  isrhm  20458  issdrg  20765  abvpropd  20812  islmhm  21022  dfprm2  21453  prmirred  21454  elocv  21648  isobs  21700  iscn2  23203  iscnp2  23204  islocfin  23482  elflim2  23929  isfcls  23974  isnghm  24688  isnmhm  24711  0plef  25639  elply  26160  dchrelbas4  27206  brslts  27754  nb3grpr  29451  ispligb  30548  isph  30893  abfmpunirn  32725  iscvm  35441  sscoid  36093  bj-pwvrelb  37205  bj-elsnb  37368  bj-ideqb  37473  bj-opelidb1ALT  37480  bj-elid5  37483  eldiophb  43189  eldioph3b  43197  eldioph4b  43239  bropabg  43751  brfvrcld2  44119  islmd  50140  iscmd  50141