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

Theorem mpbiran2 953
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.2 . 2 (𝜑 ↔ (𝜓𝜒))
2 mpbiran2.1 . . 3 𝜒
32biantru 526 . 2 (𝜓 ↔ (𝜓𝜒))
41, 3bitr4i 267 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 197  df-an 386
This theorem is referenced by:  pm5.62  957  reueq  3386  ss0b  3945  eusv1  4820  eusv2nf  4824  eusv2  4825  opthprc  5127  sosn  5149  opelres  5361  fdmrn  6021  f1cnvcnv  6066  fores  6081  f1orn  6104  funfv  6222  dfoprab2  6654  elxp7  7146  tpostpos  7317  canthwe  9417  recmulnq  9730  opelreal  9895  elreal2  9897  eqresr  9902  elnn1uz2  11709  faclbnd4lem1  13020  isprm2  15319  joindm  16924  meetdm  16938  symgbas0  17735  efgs1  18069  toptopon  20648  ist1-3  21063  perfcls  21079  prdsxmetlem  22083  rusgrprc  26356  hhsssh2  27973  choc0  28031  chocnul  28033  shlesb1i  28091  adjeu  28594  isarchi  29518  derang0  30856  brtxp  31626  brpprod  31631  dfon3  31638  brtxpsd  31640  topmeet  31998  filnetlem2  32013  filnetlem3  32014  bj-rabtrALT  32571  bj-snsetex  32595  relowlpssretop  32841  poimirlem28  33066  fdc  33170  0totbnd  33201  heiborlem3  33241  ifpid3g  37315  elintima  37423
  Copyright terms: Public domain W3C validator