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

Theorem simplbi 270
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 119 . 2  |-  ( ph  ->  ( ps  /\  ch ) )
32simpld 111 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.62dc  912  3simpa  961  xoror  1340  anxordi  1361  sbidm  1805  reurex  2619  eqimss  3119  eldifi  3166  elinel1  3230  inss1  3264  sopo  4203  wefr  4248  ordtr  4268  opelxp1  4541  relop  4657  funmo  5106  funrel  5108  funinsn  5140  fnfun  5188  ffn  5240  f1f  5296  f1of1  5332  f1ofo  5340  isof1o  5674  eqopi  6036  1st2nd2  6039  reldmtpos  6116  swoer  6423  ecopover  6493  ecopoverg  6496  fnfi  6791  casef  6939  dfplpq2  7126  enq0ref  7205  cauappcvgprlemopl  7418  cauappcvgprlemdisj  7423  caucvgprlemopl  7441  caucvgprlemdisj  7446  caucvgprprlemopl  7469  caucvgprprlemopu  7471  caucvgprprlemdisj  7474  peano1nnnn  7624  axrnegex  7651  ltxrlt  7794  1nn  8688  zre  9009  nnssz  9022  ixxss1  9627  ixxss2  9628  ixxss12  9629  iccss2  9667  rge0ssre  9700  elfzuz  9742  uzdisj  9813  nn0disj  9855  frecuzrdgtcl  10125  frecuzrdgfunlem  10132  modfsummodlemstep  11166  mertenslem2  11245  prmnn  11687  prmuz2  11707  oddpwdc  11747  sqpweven  11748  2sqpwodd  11749  phimullem  11796  hashgcdlem  11798  ctinfom  11836  ctinf  11838  topontop  12076  tpstop  12097  cntop1  12265  cntop2  12266  hmeocn  12369  isxmet2d  12412  metxmet  12419  xmstps  12521  msxms  12522  xmsxmet  12524  msmet  12525  bdxmet  12565  bj-indint  12940  bj-inf2vnlem2  12980  nninff  13009  peano4nninf  13011
  Copyright terms: Public domain W3C validator