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

Theorem mpbiran2 910
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 505 . 2  |-  ( ps  <->  ( ps  /\  ch )
)
41, 3bitr4i 252 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  pm5.62  914  reueq  3159  ss0b  3670  eusv1  4489  eusv2nf  4493  eusv2  4494  opthprc  4889  sosn  4911  opelres  5119  fdmrn  5576  f1cnvcnv  5617  fores  5632  f1orn  5654  funfv  5761  dfoprab2  6136  elxp7  6612  tpostpos  6768  dfsup2OLD  7696  canthwe  8821  recmulnq  9136  opelreal  9300  elreal2  9302  eqresr  9307  elnn1uz2  10934  faclbnd4lem1  12072  isprm2  13774  joindm  15176  meetdm  15190  symgbas0  15902  efgs1  16235  funsnfsupOLD  17673  toptopon  18541  ist1-3  18956  perfcls  18972  prdsxmetlem  19946  hhsssh2  24674  choc0  24732  chocnul  24734  shlesb1i  24792  adjeu  25296  isarchi  26202  derang0  27060  nofulllem5  27850  brtxp  27914  brpprod  27919  dfon3  27926  brtxpsd  27928  topmeet  28588  filnetlem2  28603  filnetlem3  28604  fdc  28644  0totbnd  28675  heiborlem3  28715  bj-rabtrALT  32436  bj-snsetex  32459
  Copyright terms: Public domain W3C validator