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  3639  elpwb  4559  ssdifsn  4739  brab2a  5712  elon2  6318  elovmpo  7594  eqop2  7967  iscard  9871  iscard2  9872  elnnnn0  12427  elfzo2  13565  bitsval  16335  1nprm  16590  funcpropd  17809  isfull  17819  isfth  17823  ismgmhm  18570  ismhm  18659  isghm  19094  isghmOLD  19095  ghmpropd  19135  isga  19170  oppgcntz  19243  gexdvdsi  19462  isrnghm  20326  isrhm  20363  issdrg  20673  abvpropd  20720  islmhm  20931  dfprm2  21380  prmirred  21381  elocv  21575  isobs  21627  iscn2  23123  iscnp2  23124  islocfin  23402  elflim2  23849  isfcls  23894  isnghm  24609  isnmhm  24632  0plef  25571  elply  26098  dchrelbas4  27152  brsslt  27696  nb3grpr  29327  ispligb  30421  isph  30766  abfmpunirn  32596  iscvm  35242  sscoid  35897  bj-pwvrelb  36882  bj-elsnb  37045  bj-ideqb  37143  bj-opelidb1ALT  37150  bj-elid5  37153  eldiophb  42740  eldioph3b  42748  eldioph4b  42794  bropabg  43306  brfvrcld2  43675  islmd  49660  iscmd  49661