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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  pm5.62  1017  rabtru  3626  reueq  3677  ss0b  4337  eusv1  5323  eusv2nf  5327  eusv2  5328  dfid2  5502  opthprc  5662  sosn  5684  fdmrn  6662  f1cnvcnv  6710  fores  6728  f1orn  6756  funfv  6887  dfoprab2  7365  elxp7  7898  tpostpos  8093  frrlem11  8143  canthwe  10457  opelreal  10936  elreal2  10938  eqresr  10943  elnn1uz2  12715  faclbnd4lem1  14057  isprm2  16436  joindm  18142  meetdm  18156  symgbas0  19045  toptopon  22115  ist1-3  22549  perfcls  22565  prdsxmetlem  23570  rusgrprc  28006  hhsssh2  29681  choc0  29737  chocnul  29739  shlesb1i  29797  adjeu  30300  isarchi  31485  derang0  33180  dfon3  34243  brtxpsd  34245  topmeet  34602  filnetlem2  34617  filnetlem3  34618  bj-rabtrALT  35167  bj-snsetex  35201  bj-dfid2ALT  35284  relowlpssretop  35583  poimirlem28  35853  fdc  35951  0totbnd  35979  heiborlem3  36019  cossssid  36681  cnvrefrelcoss2  36751  dfdisjALTV  36927  dfeldisj2  36932  dfeldisj3  36933  dfeldisj4  36934  disjres  36958  disjxrn  36960  dfantisymrel4  36975  dfantisymrel5  36976  antisymrelres  36977  ifpid3g  41312  elintima  41474