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  6450  enq0ref  6529  cauappcvgprlemopl  6742  cauappcvgprlemdisj  6747  caucvgprlemopl  6765  caucvgprlemdisj  6770  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemdisj  6798  peano1nnnn  6926  axrnegex  6951  ltxrlt  7083  1nn  7923  zre  8247  nnssz  8260  ixxss1  8771  ixxss2  8772  ixxss12  8773  iccss2  8811  rge0ssre  8844  elfzuz  8884  uzdisj  8953  nn0disj  8993  frecuzrdgfn  9172  bj-indint  10029  bj-inf2vnlem2  10070
  Copyright terms: Public domain W3C validator