MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpbiran2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 mpbiran2.1 . 2 𝜒
2 mpbiran2.2 . . 3 (𝜑 ↔ (𝜓𝜒))
32biancomi 463 . 2 (𝜑 ↔ (𝜒𝜓))
41, 3mpbiran 705 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm5.62  1013  rabtru  3615  reueq  3662  ss0b  4271  eusv1  5183  eusv2nf  5187  eusv2  5188  opthprc  5502  sosn  5524  fdmrn  6406  f1cnvcnv  6452  fores  6468  f1orn  6493  funfv  6617  dfoprab2  7071  elxp7  7580  tpostpos  7763  canthwe  9919  opelreal  10398  elreal2  10400  eqresr  10405  elnn1uz2  12174  faclbnd4lem1  13503  isprm2  15855  joindm  17442  meetdm  17456  symgbas0  18253  toptopon  21209  ist1-3  21641  perfcls  21657  prdsxmetlem  22661  rusgrprc  27055  hhsssh2  28738  choc0  28794  chocnul  28796  shlesb1i  28854  adjeu  29357  isarchi  30449  derang0  32025  frrlem11  32743  dfon3  32963  brtxpsd  32965  topmeet  33322  filnetlem2  33337  filnetlem3  33338  bj-rabtrALT  33824  bj-snsetex  33899  relowlpssretop  34195  poimirlem28  34470  fdc  34571  0totbnd  34602  heiborlem3  34642  cossssid  35257  cnvrefrelcoss2  35323  dfdisjALTV  35496  dfeldisj2  35501  dfeldisj3  35502  dfeldisj4  35503  disjxrn  35527  ifpid3g  39362  elintima  39502
  Copyright terms: Public domain W3C validator