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

Theorem mpbiran2 887
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 493 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 245 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm5.62  891  reueq  3133  ss0b  3659  eusv1  4720  eusv2nf  4724  eusv2  4725  opthprc  4928  sosn  4950  opelres  5154  f1cnvcnv  5650  fores  5665  f1orn  5687  funfv  5793  dfoprab2  6124  elxp7  6382  tpostpos  6502  dfsup2OLD  7451  canthwe  8531  recmulnq  8846  opelreal  9010  elreal2  9012  eqresr  9017  elnn1uz2  10557  faclbnd4lem1  11589  isprm2  13092  efgs1  15372  toptopon  17003  ist1-3  17418  perfcls  17434  prdsxmetlem  18403  hhsssh2  22775  choc0  22833  chocnul  22835  shlesb1i  22893  adjeu  23397  fdmrn  24044  isarchi  24257  derang0  24860  nofulllem5  25666  brtxp  25730  brpprod  25735  dfon3  25742  brtxpsd  25744  topmeet  26406  filnetlem2  26421  filnetlem3  26422  fdc  26462  0totbnd  26495  heiborlem3  26535  funsnfsup  26756
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 179  df-an 362
  Copyright terms: Public domain W3C validator