Theorem biadanii 818

Description: Inference associated with biadani 816. 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 816	. 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  3672  elpwb  4609  ssdifsn  4790  brab2a  5768  elon2  6374  elovmpo  7653  eqop2  8020  iscard  9972  iscard2  9973  elnnnn0  12519  elfzo2  13639  bitsval  16369  1nprm  16620  funcpropd  17855  isfull  17865  isfth  17869  ismgmhm  18621  ismhm  18707  isghm  19130  ghmpropd  19170  isga  19196  oppgcntz  19272  gexdvdsi  19492  isrnghm  20332  isrhm  20369  issdrg  20547  abvpropd  20593  islmhm  20782  dfprm2  21244  prmirred  21245  elocv  21440  isobs  21494  iscn2  22962  iscnp2  22963  islocfin  23241  elflim2  23688  isfcls  23733  isnghm  24460  isnmhm  24483  0plef  25421  elply  25944  dchrelbas4  26982  brsslt  27523  nb3grpr  28906  ispligb  29997  isph  30342  abfmpunirn  32144  iscvm  34548  sscoid  35189  bj-pwvrelb  36081  bj-elsnb  36245  bj-ideqb  36343  bj-opelidb1ALT  36350  bj-elid5  36353  eldiophb  41797  eldioph3b  41805  eldioph4b  41851  bropabg  42375  brfvrcld2  42745