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

Theorem simpl 106
Description: Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpl  |-  ( (
ph  /\  ps )  ->  ph )

Proof of Theorem simpl
StepHypRef Expression
1 ax-ia1 103 1  |-  ( (
ph  /\  ps )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-ia1 103
This theorem is referenced by:  simpli  108  simpld  109  imp  119  adantrd  268  iba  288  pm3.41  318  pm4.45im  321  prth  330  pm4.71  375  adantlr  454  adantrr  456  adantllr  458  adantlrr  460  adantrlr  462  adantrrr  464  simplll  493  simplrl  495  simprll  497  simprrl  499  anabs1  514  jcab  545  pm4.38  547  pm5.21  621  ioran  679  pm3.14  680  pm4.44  706  ordi  740  pm4.39  746  pm5.16  748  pm5.54dc  838  intnanr  850  intnanrd  852  dcan  853  dedlema  887  dedlemb  888  pm4.42r  889  prlem2  892  simp1l  939  simp2l  941  simp3l  943  3anandis  1253  xordc1  1300  anxordi  1307  falantru  1310  19.26  1386  exsimpl  1524  sbequ2  1668  sbcof2  1707  sbequilem  1735  sbequ8  1743  euan  1972  mooran1  1988  eupickbi  1998  2exeu  2008  dimatis  2033  rexim  2430  r19.26  2458  r19.40  2481  rr19.28v  2705  elrab3t  2719  eueq3dc  2737  mosubt  2740  reu6  2752  sbc2iegf  2855  sbcralt  2861  sbcrext  2862  rmob  2877  csbiebt  2913  ssab2  3051  difdif  3096  uneqin  3215  indifdir  3220  undif3ss  3225  rexm  3347  difsn  3528  opprc1  3598  unissel  3636  ssmin  3661  abssexg  3961  opelopabsb  4024  sess1  4101  ordelord  4145  onin  4150  suctr  4185  ordtriexmidlem  4272  ordtri2or2exmid  4323  tfi  4332  peano1  4344  peano2  4345  0nelxp  4399  0nelelxp  4400  brab2a  4420  mosubopt  4432  posng  4439  opabssxp  4441  ideqg  4514  relssres  4675  trin2  4743  dminss  4765  iota4an  4913  iota2  4920  fun11uni  4996  imadiflem  5005  funimaexg  5010  fneq12  5019  fvelrnb  5248  dffo4  5342  ffnfv  5350  ffvresb  5355  fmptco  5357  fcoconst  5361  fcof1  5450  isotr  5483  isopolem  5488  f1oiso  5492  acexmidlemcase  5534  ovprc1  5568  fnoprabg  5629  op1steq  5832  1stconst  5869  f1o2ndf1  5876  sprmpt2  5887  brtpos2  5896  tpostpos  5909  tposf12  5914  smores  5937  tfrlemi1  5976  freceq1  6009  freceq2  6010  frectfr  6015  omv2  6075  omsuc  6081  nnsucelsuc  6100  nntri3  6105  nnaordi  6111  nnmordi  6119  nnm00  6132  ecexr  6141  ertr  6151  swoer  6164  erth  6180  ecelqsdm  6206  iinerm  6208  ecinxp  6211  erovlem  6228  dom3  6286  phpelm  6358  nnwetri  6384  supubti  6404  supisoex  6412  ordiso2  6414  dmaddpqlem  6532  distrnqg  6542  ltanqi  6557  ltmnqi  6558  ltaddnq  6562  ltrnqg  6575  ltnnnq  6578  enq0sym  6587  addnq0mo  6602  mulnq0mo  6603  addnnnq0  6604  distrnq0  6614  prarloclemn  6654  prarloc  6658  ltdfpr  6661  genplt2i  6665  addnqprl  6684  addnqpru  6685  nqprl  6706  appdivnq  6718  1idprl  6745  1idpru  6746  ltexpri  6768  recexpr  6793  cauappcvgprlemdisj  6806  archrecpr  6819  addsrmo  6885  mulsrmo  6886  addsrpr  6887  mulsrpr  6888  0idsr  6909  1idsr  6910  archsr  6923  prsradd  6927  prsrlt  6928  caucvgsr  6943  elrealeu  6963  muladd11r  7229  negeu  7264  pncan  7279  pncan3  7281  negsub  7321  addid0  7442  posdif  7523  ltnegcon1  7531  subge0  7543  suble0  7544  lesub0  7547  reapval  7640  reapneg  7661  ap0gt0  7702  recextlem1  7705  div0ap  7752  recrecap  7759  rec11ap  7760  recgt0  7890  mulgt1  7903  lerec2  7929  recp1lt1  7939  recreclt  7940  ledivp1  7943  nnsub  8027  avglt1  8219  nnrecl  8236  nnnn0addcl  8268  elnn0nn  8280  nn0ge2m1nn  8298  zaddcl  8341  eluzadd  8596  divfnzn  8652  qaddcl  8666  qreccl  8673  cnref1o  8679  ge0p1rp  8711  divlt1lt  8747  divle1le  8748  addlelt  8785  xrre3  8835  xltnegi  8848  ixxssixx  8871  iccshftr  8962  iccshftl  8964  iccdil  8966  icccntr  8968  zltaddlt1le  8974  elfz2  8982  peano2fzr  9002  fzdcel  9005  fzsplit2  9015  fzaddel  9023  fzrev2  9048  fzrev2i  9049  fzrev3  9050  elfz1b  9053  fseq1p1m1  9057  uzsubfz0  9087  fzosubel3  9153  eluzgtdifelfzo  9154  fzofzp1b  9185  elfzomelpfzo  9188  fvinim0ffz  9197  qbtwnxr  9213  ico0  9217  flqge  9231  flqlt  9232  flqltnz  9236  flqbi2  9240  flqaddz  9246  flqmulnn0  9248  intfracq  9269  flqdiv  9270  q0mod  9304  q1mod  9305  mulp1mod1  9314  q2txmodxeq0  9333  modfzo0difsn  9344  frec2uzuzd  9351  frec2uzltd  9352  frec2uzrand  9354  iseqsplit  9401  iseqcaopr  9405  expivallem  9420  expival  9421  expinnval  9422  exp1  9425  expcl2lemap  9431  rpexpcl  9438  expnegzap  9453  mulexp  9458  mulexpzap  9459  leexp2r  9473  leexp1a  9474  sq11  9491  subsq  9524  binom2  9528  binom3  9533  zesq  9534  bernneq  9536  sq11ap  9582  facwordi  9607  facubnd  9612  facavg  9613  bcval  9616  ibcval5  9630  shftfvalg  9646  ovshftex  9647  shftdm  9650  shftfib  9651  shftval  9653  shftf  9658  crre  9684  cjexp  9720  cjreim2  9731  uzin2  9813  rexuz3  9816  resqrexlemgt0  9846  resqrex  9852  sqrtgt0  9860  sqrtsq  9870  sqrtmsq  9871  absrpclap  9887  absext  9889  absmul  9895  absid  9897  absexp  9905  nn0abscl  9911  abslt  9914  absle  9915  recvalap  9923  abstri  9930  caubnd2  9943  qdenre  10028  climconst2  10042  climmpt  10051  climres  10054  climcaucn  10100  sumeq1  10104  dvdsdc  10115  iddvdsexp  10130  dvdsadd  10149  dvds1  10164  odd2np1  10183  oddm1even  10185  m1exp1  10212  pw2dvdslemn  10232  oddpwdclemdc  10240  bj-indind  10422  bj-omtrans  10447  bj-inf2vnlem1  10461  sscoll2  10479  qdencn  10490
  Copyright terms: Public domain W3C validator