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  3048  ss0b  3572  pwundifOLD  4403  eusv1  4631  eusv2nf  4635  eusv2  4636  opthprc  4839  sosn  4862  opelres  5063  f1cnvcnv  5551  fores  5566  f1orn  5588  funfv  5693  dfoprab2  6021  elxp7  6279  tpostpos  6396  dfsup2OLD  7343  canthwe  8420  recmulnq  8735  opelreal  8899  elreal2  8901  eqresr  8906  elnn1uz2  10445  faclbnd4lem1  11471  isprm2  12974  efgs1  15254  toptopon  16888  ist1-3  17294  perfcls  17310  prdsxmetlem  18145  hhsssh2  22281  choc0  22339  chocnul  22341  shlesb1i  22399  adjeu  22903  fdmrn  23563  derang0  24424  nofulllem5  25186  brtxp  25246  brpprod  25251  dfon3  25258  brtxpsd  25260  topmeet  25905  filnetlem2  25920  filnetlem3  25921  fdc  26047  0totbnd  26088  heiborlem3  26128  funsnfsup  26353
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