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 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  3674  elpwb  4611  ssdifsn  4792  brab2a  5770  elon2  6376  elovmpo  7651  eqop2  8018  iscard  9970  iscard2  9971  elnnnn0  12515  elfzo2  13635  bitsval  16365  1nprm  16616  funcpropd  17851  isfull  17861  isfth  17865  ismhm  18673  isghm  19092  ghmpropd  19130  isga  19155  oppgcntz  19231  gexdvdsi  19451  isrhm  20257  issdrg  20404  abvpropd  20450  islmhm  20638  dfprm2  21043  prmirred  21044  elocv  21221  isobs  21275  iscn2  22742  iscnp2  22743  islocfin  23021  elflim2  23468  isfcls  23513  isnghm  24240  isnmhm  24263  0plef  25189  elply  25709  dchrelbas4  26746  brsslt  27287  nb3grpr  28639  ispligb  29730  isph  30075  abfmpunirn  31877  iscvm  34250  sscoid  34885  bj-pwvrelb  35778  bj-elsnb  35942  bj-ideqb  36040  bj-opelidb1ALT  36047  bj-elid5  36050  eldiophb  41495  eldioph3b  41503  eldioph4b  41549  bropabg  42073  brfvrcld2  42443  ismgmhm  46553  isrnghm  46690