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  887  3simpa  936  xoror  1311  anxordi  1332  sbidm  1773  reurex  2568  eqimss  3052  eldifi  3095  elinel1  3159  inss1  3193  sopo  4076  wefr  4121  ordtr  4141  opelxp1  4403  relop  4514  funmo  4947  funrel  4949  funinsn  4979  fnfun  5027  ffn  5077  f1f  5123  f1of1  5156  f1ofo  5164  isof1o  5478  eqopi  5829  1st2nd2  5832  reldmtpos  5902  swoer  6200  ecopover  6270  ecopoverg  6273  fnfi  6446  dfplpq2  6606  enq0ref  6685  cauappcvgprlemopl  6898  cauappcvgprlemdisj  6903  caucvgprlemopl  6921  caucvgprlemdisj  6926  caucvgprprlemopl  6949  caucvgprprlemopu  6951  caucvgprprlemdisj  6954  peano1nnnn  7082  axrnegex  7107  ltxrlt  7245  1nn  8117  zre  8436  nnssz  8449  ixxss1  9003  ixxss2  9004  ixxss12  9005  iccss2  9043  rge0ssre  9076  elfzuz  9117  uzdisj  9186  nn0disj  9225  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  prmnn  10636  prmuz2  10656  oddpwdc  10696  sqpweven  10697  2sqpwodd  10698  bj-indint  10884  bj-inf2vnlem2  10924
  Copyright terms: Public domain W3C validator