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  3647  reueq  3699  ss0b  4354  eusv1  5333  eusv2nf  5337  eusv2  5338  dfid2  5520  opthprc  5687  sosn  5710  fdmrn  6687  f1cnvcnv  6733  fores  6750  f1orn  6778  funfv  6914  dfoprab2  7411  elxp7  7966  tpostpos  8186  frrlem11  8236  canthwe  10564  opelreal  11043  elreal2  11045  eqresr  11050  elnn1uz2  12844  faclbnd4lem1  14218  isprm2  16611  joindm  18297  meetdm  18311  symgbas0  19286  toptopon  22820  ist1-3  23252  perfcls  23268  prdsxmetlem  24272  eln0s  28274  rusgrprc  29554  hhsssh2  31232  choc0  31288  chocnul  31290  shlesb1i  31348  adjeu  31851  isarchi  33134  derang0  35141  dfon3  35865  brtxpsd  35867  topmeet  36337  filnetlem2  36352  filnetlem3  36353  bj-rabtrALT  36904  bj-snsetex  36936  bj-dfid2ALT  37038  relowlpssretop  37337  poimirlem28  37627  fdc  37724  0totbnd  37752  heiborlem3  37792  cossssid  38443  cnvrefrelcoss2  38513  dfdisjALTV  38690  dfeldisj2  38695  dfeldisj3  38696  dfeldisj4  38697  disjres  38721  disjxrn  38723  dfantisymrel4  38738  dfantisymrel5  38739  antisymrelres  38740  ifpid3g  43465  elintima  43626  brpermmodel  44977  0funcALT  49074