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  3641  reueq  3692  ss0b  4350  eusv1  5331  eusv2nf  5335  eusv2  5336  dfid2  5516  opthprc  5683  sosn  5706  fdmrn  6687  f1cnvcnv  6733  fores  6750  f1orn  6778  funfv  6915  dfoprab2  7410  elxp7  7962  tpostpos  8182  frrlem11  8232  canthwe  10549  opelreal  11028  elreal2  11030  eqresr  11035  elnn1uz2  12825  faclbnd4lem1  14202  isprm2  16595  joindm  18281  meetdm  18295  symgbas0  19303  toptopon  22833  ist1-3  23265  perfcls  23281  prdsxmetlem  24284  eln0s  28288  rusgrprc  29571  hhsssh2  31252  choc0  31308  chocnul  31310  shlesb1i  31368  adjeu  31871  isarchi  33158  derang0  35234  dfon3  35955  brtxpsd  35957  topmeet  36429  filnetlem2  36444  filnetlem3  36445  bj-rabtrALT  36996  bj-snsetex  37028  bj-dfid2ALT  37130  relowlpssretop  37429  poimirlem28  37709  fdc  37806  0totbnd  37834  heiborlem3  37874  cossssid  38590  cnvrefrelcoss2  38650  dfdisjALTV  38832  dfeldisj2  38837  dfeldisj3  38838  dfeldisj4  38839  disjres  38863  disjxrn  38865  dfantisymrel4  38880  dfantisymrel5  38881  antisymrelres  38882  ifpid3g  43610  elintima  43771  brpermmodel  45121  0funcALT  49214