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

Theorem mpbiran2 709
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 466 . 2 (𝜑 ↔ (𝜒𝜓))
41, 3mpbiran 708 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  pm5.62  1016  rabtru  3663  reueq  3714  ss0b  4334  eusv1  5279  eusv2nf  5283  eusv2  5284  opthprc  5603  sosn  5625  fdmrn  6528  f1cnvcnv  6575  fores  6591  f1orn  6616  funfv  6741  dfoprab2  7205  elxp7  7719  tpostpos  7908  canthwe  10071  opelreal  10550  elreal2  10552  eqresr  10557  elnn1uz2  12322  faclbnd4lem1  13658  isprm2  16024  joindm  17613  meetdm  17627  symgbas0  18517  toptopon  21525  ist1-3  21957  perfcls  21973  prdsxmetlem  22978  rusgrprc  27383  hhsssh2  29056  choc0  29112  chocnul  29114  shlesb1i  29172  adjeu  29675  isarchi  30843  derang0  32473  frrlem11  33190  dfon3  33410  brtxpsd  33412  topmeet  33769  filnetlem2  33784  filnetlem3  33785  bj-rabtrALT  34317  bj-snsetex  34343  relowlpssretop  34726  poimirlem28  35030  fdc  35128  0totbnd  35156  heiborlem3  35196  cossssid  35812  cnvrefrelcoss2  35878  dfdisjALTV  36051  dfeldisj2  36056  dfeldisj3  36057  dfeldisj4  36058  disjxrn  36082  ifpid3g  40116  elintima  40270
  Copyright terms: Public domain W3C validator