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

Theorem mpbiran2 885
Description: Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
Hypotheses
Ref Expression
mpbiran2.1  |-  ch
mpbiran2.2  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
mpbiran2  |-  ( ph  <->  ps )

Proof of Theorem mpbiran2
StepHypRef Expression
1 mpbiran2.2 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
2 mpbiran2.1 . . 3  |-  ch
32biantru 491 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 243 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm5.62  889  reueq  2962  ss0b  3484  pwundifOLD  4301  eusv1  4528  eusv2nf  4532  eusv2  4533  opthprc  4736  sosn  4759  opelres  4960  f1cnvcnv  5445  fores  5460  f1orn  5482  funfv  5586  dfoprab2  5895  elxp7  6152  tpostpos  6254  dfsup2OLD  7196  canthwe  8273  recmulnq  8588  opelreal  8752  elreal2  8754  eqresr  8759  elnn1uz2  10294  faclbnd4lem1  11306  isprm2  12766  efgs1  15044  toptopon  16671  ist1-3  17077  perfcls  17093  prdsxmetlem  17932  hhsssh2  21847  choc0  21905  chocnul  21907  shlesb1i  21965  adjeu  22469  fdmrn  23035  derang0  23700  nofulllem5  24360  brtxp  24420  brpprod  24425  dfon3  24432  brtxpsd  24434  cmpdom  25143  cmppar2  25972  topmeet  26313  filnetlem2  26328  filnetlem3  26329  fdc  26455  0totbnd  26497  heiborlem3  26537  funsnfsup  26762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator