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 229	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  elab4g  3683  elpwb  4618  ssdifsn  4800  brab2a  5779  elon2  6391  elovmpo  7676  eqop2  8054  iscard  10025  iscard2  10026  elnnnn0  12577  elfzo2  13699  bitsval  16445  1nprm  16701  funcpropd  17943  isfull  17953  isfth  17957  ismgmhm  18710  ismhm  18796  isghm  19231  isghmOLD  19232  ghmpropd  19272  isga  19307  oppgcntz  19383  gexdvdsi  19603  isrnghm  20445  isrhm  20482  issdrg  20789  abvpropd  20836  islmhm  21027  dfprm2  21485  prmirred  21486  elocv  21686  isobs  21740  iscn2  23256  iscnp2  23257  islocfin  23535  elflim2  23982  isfcls  24027  isnghm  24754  isnmhm  24777  0plef  25715  elply  26245  dchrelbas4  27295  brsslt  27838  nb3grpr  29341  ispligb  30433  isph  30778  abfmpunirn  32595  iscvm  35134  sscoid  35784  bj-pwvrelb  36652  bj-elsnb  36815  bj-ideqb  36913  bj-opelidb1ALT  36920  bj-elid5  36923  eldiophb  42485  eldioph3b  42493  eldioph4b  42539  bropabg  43060  brfvrcld2  43430