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  3651  reueq  3703  ss0b  4361  eusv1  5367  eusv2nf  5371  eusv2  5372  dfid2  5563  opthprc  5730  sosn  5753  fdmrn  6744  f1cnvcnv  6792  fores  6809  f1orn  6838  funfv  6975  dfoprab2  7481  elxp7  8030  tpostpos  8251  frrlem11  8302  canthwe  10654  opelreal  11133  elreal2  11135  eqresr  11140  elnn1uz2  12967  faclbnd4lem1  14349  isprm2  16765  joindm  18454  meetdm  18468  symgbas0  19490  toptopon  23111  ist1-3  23543  perfcls  23559  prdsxmetlem  24562  eln0s  28591  rusgrprc  29977  hhsssh2  31659  choc0  31715  chocnul  31717  shlesb1i  31775  adjeu  32278  isarchi  33533  vonf1osev  35620  derang0  35682  dfon3  36403  brtxpsd  36405  topmeet  36916  filnetlem2  36931  filnetlem3  36932  bj-rabtrALT  37608  bj-snsetex  37640  bj-dfid2ALT  37742  relowlpssretop  38051  poimirlem28  38340  fdc  38437  0totbnd  38465  heiborlem3  38505  cossssid  39247  cnvrefrelcoss2  39307  dfdisjALTV  39488  dfeldisj2  39500  dfeldisj3  39501  dfeldisj4  39502  disjqmap2  39516  disjres  39534  disjxrn  39536  dfantisymrel4  39554  dfantisymrel5  39555  antisymrelres  39556  ifpid3g  44259  elintima  44420  brpermmodel  45753  0funcALT  49907