Theorem biadanii 821

Description: Inference associated with biadani 819. 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 819	. 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  3653  elpwb  4574  ssdifsn  4755  brab2a  5735  elon2  6346  elovmpo  7637  eqop2  8014  iscard  9935  iscard2  9936  elnnnn0  12492  elfzo2  13630  bitsval  16401  1nprm  16656  funcpropd  17871  isfull  17881  isfth  17885  ismgmhm  18630  ismhm  18719  isghm  19154  isghmOLD  19155  ghmpropd  19195  isga  19230  oppgcntz  19303  gexdvdsi  19520  isrnghm  20357  isrhm  20394  issdrg  20704  abvpropd  20751  islmhm  20941  dfprm2  21390  prmirred  21391  elocv  21584  isobs  21636  iscn2  23132  iscnp2  23133  islocfin  23411  elflim2  23858  isfcls  23903  isnghm  24618  isnmhm  24641  0plef  25580  elply  26107  dchrelbas4  27161  brsslt  27704  nb3grpr  29316  ispligb  30413  isph  30758  abfmpunirn  32583  iscvm  35253  sscoid  35908  bj-pwvrelb  36893  bj-elsnb  37056  bj-ideqb  37154  bj-opelidb1ALT  37161  bj-elid5  37164  eldiophb  42752  eldioph3b  42760  eldioph4b  42806  bropabg  43319  brfvrcld2  43688  islmd  49658  iscmd  49659