Theorem mpbiran2 706

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 705	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  1015  rabtru  3622  reueq  3675  ss0b  4336  eusv1  5317  eusv2nf  5321  eusv2  5322  dfid2  5490  opthprc  5650  sosn  5672  fdmrn  6628  f1cnvcnv  6676  fores  6694  f1orn  6722  funfv  6849  dfoprab2  7324  elxp7  7852  tpostpos  8046  frrlem11  8096  canthwe  10391  opelreal  10870  elreal2  10872  eqresr  10877  elnn1uz2  12647  faclbnd4lem1  13988  isprm2  16368  joindm  18074  meetdm  18088  symgbas0  18977  toptopon  22047  ist1-3  22481  perfcls  22497  prdsxmetlem  23502  rusgrprc  27938  hhsssh2  29611  choc0  29667  chocnul  29669  shlesb1i  29727  adjeu  30230  isarchi  31415  derang0  33110  dfon3  34173  brtxpsd  34175  topmeet  34532  filnetlem2  34547  filnetlem3  34548  bj-rabtrALT  35098  bj-snsetex  35132  bj-dfid2ALT  35215  relowlpssretop  35514  poimirlem28  35784  fdc  35882  0totbnd  35910  heiborlem3  35950  cossssid  36564  cnvrefrelcoss2  36630  dfdisjALTV  36803  dfeldisj2  36808  dfeldisj3  36809  dfeldisj4  36810  disjxrn  36834  ifpid3g  41061  elintima  41214