ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simplbi Unicode version

Theorem simplbi 259
Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
Hypothesis
Ref Expression
simplbi.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
simplbi  |-  ( ph  ->  ps )

Proof of Theorem simplbi
StepHypRef Expression
1 simplbi.1 . . 3  |-  ( ph  <->  ( ps  /\  ch )
)
21biimpi 113 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 105 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  pm5.62dc  852  3simpa  901  xoror  1270  anxordi  1291  sbidm  1731  reurex  2523  eqimss  2997  pssss  3039  eldifi  3066  inss1  3157  sopo  4050  wefr  4095  ordtr  4115  opelxp1  4377  relop  4486  funmo  4917  funrel  4919  fnfun  4996  ffn  5046  f1f  5092  f1of1  5125  f1ofo  5133  isof1o  5447  eqopi  5798  1st2nd2  5801  reldmtpos  5868  swoer  6134  ecopover  6204  ecopoverg  6207  dfplpq2  6452  enq0ref  6531  cauappcvgprlemopl  6744  cauappcvgprlemdisj  6749  caucvgprlemopl  6767  caucvgprlemdisj  6772  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemdisj  6800  peano1nnnn  6928  axrnegex  6953  ltxrlt  7085  1nn  7925  zre  8249  nnssz  8262  ixxss1  8773  ixxss2  8774  ixxss12  8775  iccss2  8813  rge0ssre  8846  elfzuz  8886  uzdisj  8955  nn0disj  8995  frecuzrdgfn  9198  bj-indint  10055  bj-inf2vnlem2  10096
  Copyright terms: Public domain W3C validator