Theorem biadanii 827

Description: Inference associated with biadani 825. 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 825	. 2 ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒)))
4	1, 3	mpbi 231	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  elab4g  3621  elpwb  4537  ssdifsn  4721  brab2a  5711  elon2  6321  elovmpo  7601  eqop2  7974  iscard  9890  iscard2  9891  elnnnn0  12471  elfzo2  13607  bitsval  16384  1nprm  16639  funcpropd  17860  isfull  17870  isfth  17874  ismgmhm  18655  ismhm  18744  isghm  19181  isghmOLD  19182  ghmpropd  19222  isga  19257  oppgcntz  19330  gexdvdsi  19549  isrnghm  20412  isrhm  20449  issdrg  20760  abvpropd  20807  islmhm  21017  dfprm2  21448  prmirred  21449  elocv  21643  isobs  21695  iscn2  23221  iscnp2  23222  islocfin  23500  elflim2  23947  isfcls  23992  isnghm  24706  isnmhm  24729  0plef  25657  elply  26178  dchrelbas4  27224  brslts  27772  nb3grpr  29469  ispligb  30566  isph  30911  abfmpunirn  32744  iscvm  35487  sscoid  36139  bj-pwvrelb  37251  bj-elsnb  37414  bj-ideqb  37519  bj-opelidb1ALT  37526  bj-elid5  37529  eldiophb  43206  eldioph3b  43214  eldioph4b  43256  bropabg  43768  brfvrcld2  44136  islmd  50155  iscmd  50156