Theorem mpbiran2 723

Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Hypotheses

Ref	Expression
mpbiran2.1	⊢ 𝜒
mpbiran2.2	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
mpbiran2	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem mpbiran2

Step	Hyp	Ref	Expression
1		mpbiran2.1	. 2 ⊢ 𝜒
2		mpbiran2.2	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	2	biancomi 468	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 722	1 ⊢ (𝜑 ↔ 𝜓)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.62  1036  rabtru  3646  reueq  3698  ss0b  4354  eusv1  5357  eusv2nf  5361  eusv2  5362  dfid2  5552  opthprc  5719  sosn  5743  fdmrn  6763  f1cnvcnv  6811  fores  6828  f1orn  6857  funfv  6995  dfoprab2  7501  elxp7  8060  tpostpos  8291  frrlem11  8342  canthwe  10763  opelreal  11242  elreal2  11244  eqresr  11249  elnn1uz2  13079  faclbnd4lem1  14464  isprm2  16886  joindm  18576  meetdm  18590  symgbas0  19633  toptopon  23265  ist1-3  23697  perfcls  23713  prdsxmetlem  24717  eln0s  28777  rusgrprc  30201  hhsssh2  31902  choc0  31958  chocnul  31960  shlesb1i  32018  adjeu  32521  isarchi  33813  vonf1osev  36040  derang0  36101  dfon3  36832  brtxpsd  36834  topmeet  37330  filnetlem2  37345  filnetlem3  37346  bj-rabtrALT  38022  bj-snsetex  38054  bj-dfid2ALT  38171  relowlpssretop  38479  poimirlem28  38758  fdc  38871  0totbnd  38899  heiborlem3  38939  cossssid  39681  cnvrefrelcoss2  39741  dfdisjALTV  39922  dfeldisj2  39934  dfeldisj3  39935  dfeldisj4  39936  disjqmap2  39950  disjres  39968  disjxrn  39970  dfantisymrel4  39988  dfantisymrel5  39989  antisymrelres  39990  ifpid3g  44685  elintima  44845  brpermmodel  46188  0funcALT  50408