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  3647  elpwb  4567  ssdifsn  4748  brab2a  5724  elon2  6331  elovmpo  7614  eqop2  7990  iscard  9904  iscard2  9905  elnnnn0  12461  elfzo2  13599  bitsval  16370  1nprm  16625  funcpropd  17844  isfull  17854  isfth  17858  ismgmhm  18605  ismhm  18694  isghm  19129  isghmOLD  19130  ghmpropd  19170  isga  19205  oppgcntz  19278  gexdvdsi  19497  isrnghm  20361  isrhm  20398  issdrg  20708  abvpropd  20755  islmhm  20966  dfprm2  21415  prmirred  21416  elocv  21610  isobs  21662  iscn2  23158  iscnp2  23159  islocfin  23437  elflim2  23884  isfcls  23929  isnghm  24644  isnmhm  24667  0plef  25606  elply  26133  dchrelbas4  27187  brsslt  27731  nb3grpr  29362  ispligb  30456  isph  30801  abfmpunirn  32626  iscvm  35239  sscoid  35894  bj-pwvrelb  36879  bj-elsnb  37042  bj-ideqb  37140  bj-opelidb1ALT  37147  bj-elid5  37150  eldiophb  42738  eldioph3b  42746  eldioph4b  42792  bropabg  43305  brfvrcld2  43674  islmd  49647  iscmd  49648