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  1021  rabtru  3689  reueq  3743  ss0b  4401  eusv1  5391  eusv2nf  5395  eusv2  5396  dfid2  5580  opthprc  5749  sosn  5772  fdmrn  6767  f1cnvcnv  6813  fores  6830  f1orn  6858  funfv  6996  dfoprab2  7491  elxp7  8049  tpostpos  8271  frrlem11  8321  canthwe  10691  opelreal  11170  elreal2  11172  eqresr  11177  elnn1uz2  12967  faclbnd4lem1  14332  isprm2  16719  joindm  18420  meetdm  18434  symgbas0  19406  toptopon  22923  ist1-3  23357  perfcls  23373  prdsxmetlem  24378  eln0s  28358  rusgrprc  29608  hhsssh2  31289  choc0  31345  chocnul  31347  shlesb1i  31405  adjeu  31908  isarchi  33189  derang0  35174  dfon3  35893  brtxpsd  35895  topmeet  36365  filnetlem2  36380  filnetlem3  36381  bj-rabtrALT  36932  bj-snsetex  36964  bj-dfid2ALT  37066  relowlpssretop  37365  poimirlem28  37655  fdc  37752  0totbnd  37780  heiborlem3  37820  cossssid  38468  cnvrefrelcoss2  38538  dfdisjALTV  38714  dfeldisj2  38719  dfeldisj3  38720  dfeldisj4  38721  disjres  38745  disjxrn  38747  dfantisymrel4  38762  dfantisymrel5  38763  antisymrelres  38764  ifpid3g  43505  elintima  43666  0funcALT  48921