Theorem mpbiran2 708

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm5.62  1015  rabtru  3676  reueq  3727  ss0b  4350  eusv1  5283  eusv2nf  5287  eusv2  5288  opthprc  5610  sosn  5632  fdmrn  6532  f1cnvcnv  6578  fores  6594  f1orn  6619  funfv  6744  dfoprab2  7206  elxp7  7718  tpostpos  7906  canthwe  10067  opelreal  10546  elreal2  10548  eqresr  10553  elnn1uz2  12319  faclbnd4lem1  13647  isprm2  16020  joindm  17607  meetdm  17621  symgbas0  18511  toptopon  21519  ist1-3  21951  perfcls  21967  prdsxmetlem  22972  rusgrprc  27366  hhsssh2  29041  choc0  29097  chocnul  29099  shlesb1i  29157  adjeu  29660  isarchi  30806  derang0  32411  frrlem11  33128  dfon3  33348  brtxpsd  33350  topmeet  33707  filnetlem2  33722  filnetlem3  33723  bj-rabtrALT  34244  bj-snsetex  34270  relowlpssretop  34639  poimirlem28  34914  fdc  35014  0totbnd  35045  heiborlem3  35085  cossssid  35701  cnvrefrelcoss2  35767  dfdisjALTV  35940  dfeldisj2  35945  dfeldisj3  35946  dfeldisj4  35947  disjxrn  35971  ifpid3g  39851  elintima  39991