Theorem mpbiran2 710

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 462	. 2 ⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))
4	1, 3	mpbiran 709	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.62  1020  rabtru  3644  reueq  3695  ss0b  4353  eusv1  5336  eusv2nf  5340  eusv2  5341  dfid2  5521  opthprc  5688  sosn  5711  fdmrn  6693  f1cnvcnv  6739  fores  6756  f1orn  6784  funfv  6921  dfoprab2  7416  elxp7  7968  tpostpos  8188  frrlem11  8238  canthwe  10562  opelreal  11041  elreal2  11043  eqresr  11048  elnn1uz2  12838  faclbnd4lem1  14216  isprm2  16609  joindm  18296  meetdm  18310  symgbas0  19318  toptopon  22861  ist1-3  23293  perfcls  23309  prdsxmetlem  24312  eln0s  28357  rusgrprc  29664  hhsssh2  31345  choc0  31401  chocnul  31403  shlesb1i  31461  adjeu  31964  isarchi  33264  derang0  35363  dfon3  36084  brtxpsd  36086  topmeet  36558  filnetlem2  36573  filnetlem3  36574  bj-rabtrALT  37132  bj-snsetex  37164  bj-dfid2ALT  37266  relowlpssretop  37565  poimirlem28  37845  fdc  37942  0totbnd  37970  heiborlem3  38010  cossssid  38726  cnvrefrelcoss2  38786  dfdisjALTV  38968  dfeldisj2  38973  dfeldisj3  38974  dfeldisj4  38975  disjres  38999  disjxrn  39001  dfantisymrel4  39016  dfantisymrel5  39017  antisymrelres  39018  ifpid3g  43729  elintima  43890  brpermmodel  45240  0funcALT  49329