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 397

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 398

This theorem is referenced by:  elab4g  3627  elpwb  4559  ssdifsn  4739  brab2a  5715  elon2  6317  elovmpo  7580  eqop2  7946  iscard  9836  iscard2  9837  elnnnn0  12381  elfzo2  13495  bitsval  16230  1nprm  16481  funcpropd  17713  isfull  17723  isfth  17727  ismhm  18529  isghm  18930  ghmpropd  18968  isga  18993  oppgcntz  19067  gexdvdsi  19284  isrhm  20059  issdrg  20167  abvpropd  20207  islmhm  20394  dfprm2  20800  prmirred  20801  elocv  20978  isobs  21032  iscn2  22494  iscnp2  22495  islocfin  22773  elflim2  23220  isfcls  23265  isnghm  23992  isnmhm  24015  0plef  24941  elply  25461  dchrelbas4  26496  brsslt  27030  nb3grpr  28037  ispligb  29126  isph  29471  abfmpunirn  31274  iscvm  33518  sscoid  34352  bj-pwvrelb  35219  bj-elsnb  35386  bj-ideqb  35484  bj-opelidb1ALT  35491  bj-elid5  35494  eldiophb  40892  eldioph3b  40900  eldioph4b  40946  bropabg  41392  brfvrcld2  41673  ismgmhm  45755  isrnghm  45868