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

Theorem simplbi 268
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 118 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 110 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.62dc  891  3simpa  940  xoror  1315  anxordi  1336  sbidm  1779  reurex  2580  eqimss  3078  eldifi  3122  elinel1  3186  inss1  3220  sopo  4140  wefr  4185  ordtr  4205  opelxp1  4471  relop  4586  funmo  5030  funrel  5032  funinsn  5063  fnfun  5111  ffn  5161  f1f  5216  f1of1  5252  f1ofo  5260  isof1o  5586  eqopi  5942  1st2nd2  5945  reldmtpos  6018  swoer  6318  ecopover  6388  ecopoverg  6391  fnfi  6644  casef  6777  dfplpq2  6911  enq0ref  6990  cauappcvgprlemopl  7203  cauappcvgprlemdisj  7208  caucvgprlemopl  7226  caucvgprlemdisj  7231  caucvgprprlemopl  7254  caucvgprprlemopu  7256  caucvgprprlemdisj  7259  peano1nnnn  7387  axrnegex  7412  ltxrlt  7550  1nn  8431  zre  8752  nnssz  8765  ixxss1  9320  ixxss2  9321  ixxss12  9322  iccss2  9360  rge0ssre  9393  elfzuz  9434  uzdisj  9503  nn0disj  9545  frecuzrdgtcl  9815  frecuzrdgfunlem  9822  modfsummodlemstep  10847  mertenslem2  10926  prmnn  11366  prmuz2  11386  oddpwdc  11426  sqpweven  11427  2sqpwodd  11428  phimullem  11475  hashgcdlem  11477  topontop  11566  bj-indint  11781  bj-inf2vnlem2  11821  nninff  11849  peano4nninf  11851
  Copyright terms: Public domain W3C validator