Theorem mpbiran2 707

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 706	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm5.62  1016  rabtru  3680  reueq  3733  ss0b  4397  eusv1  5389  eusv2nf  5393  eusv2  5394  dfid2  5576  opthprc  5740  sosn  5762  fdmrn  6749  f1cnvcnv  6797  fores  6815  f1orn  6843  funfv  6978  dfoprab2  7470  elxp7  8013  tpostpos  8234  frrlem11  8284  canthwe  10649  opelreal  11128  elreal2  11130  eqresr  11135  elnn1uz2  12914  faclbnd4lem1  14258  isprm2  16624  joindm  18333  meetdm  18347  symgbas0  19298  toptopon  22640  ist1-3  23074  perfcls  23090  prdsxmetlem  24095  rusgrprc  29115  hhsssh2  30791  choc0  30847  chocnul  30849  shlesb1i  30907  adjeu  31410  isarchi  32599  derang0  34459  dfon3  35169  brtxpsd  35171  topmeet  35553  filnetlem2  35568  filnetlem3  35569  bj-rabtrALT  36115  bj-snsetex  36148  bj-dfid2ALT  36250  relowlpssretop  36549  poimirlem28  36820  fdc  36917  0totbnd  36945  heiborlem3  36985  cossssid  37641  cnvrefrelcoss2  37711  dfdisjALTV  37887  dfeldisj2  37892  dfeldisj3  37893  dfeldisj4  37894  disjres  37918  disjxrn  37920  dfantisymrel4  37935  dfantisymrel5  37936  antisymrelres  37937  ifpid3g  42546  elintima  42707