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

Theorem simpl 107
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 104 1  |-  ( (
ph  /\  ps )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-ia1 104
This theorem is referenced by:  simpli  109  simpld  110  imp  122  adantrd  273  iba  294  pm3.41  324  pm4.45im  327  prth  336  pm4.71  381  adantlr  461  adantrr  463  adantllr  465  adantlrr  467  adantrlr  469  adantrrr  471  simplll  500  simplrl  502  simprll  504  simprrl  506  anabs1  537  jcab  568  pm4.38  570  pm5.21  644  ioran  702  pm3.14  703  pm4.44  729  ordi  763  pm4.39  769  pm5.16  771  pm5.54dc  861  intnanr  873  intnanrd  875  dcan  876  dedlema  911  dedlemb  912  pm4.42r  913  prlem2  916  simp1l  963  simp2l  965  simp3l  967  3anandis  1279  xordc1  1325  anxordi  1332  falantru  1335  19.26  1411  exsimpl  1549  sbequ2  1694  sbcof2  1733  sbequilem  1761  sbequ8  1770  euan  1999  mooran1  2015  eupickbi  2025  2exeu  2035  dimatis  2060  rexim  2461  r19.26  2491  r19.40  2514  rr19.28v  2743  elrab3t  2757  eueq3dc  2776  mosubt  2779  reu6  2791  sbc2iegf  2894  sbcralt  2900  sbcrext  2901  rmob  2916  csbiebt  2952  ssab2  3088  difdif  3108  uneqin  3232  indifdir  3237  undif3ss  3242  rexm  3358  difsn  3543  opprc1  3613  unissel  3651  ssmin  3676  abssexg  3976  undifexmid  3985  exmidundif  3992  opelopabsb  4044  sess1  4121  ordelord  4165  onin  4170  suctr  4205  ordtriexmidlem  4292  ordtri2or2exmid  4343  tfi  4352  peano1  4364  peano2  4365  0nelxp  4419  0nelelxp  4420  brab2a  4440  mosubopt  4452  posng  4459  opabssxp  4461  ideqg  4536  relssres  4697  trin2  4767  dminss  4789  iota4an  4937  iota2  4944  fun11uni  5021  imadiflem  5030  funimaexg  5035  fneq12  5044  fvelrnb  5275  dffo4  5369  ffnfv  5377  ffvresb  5382  fmptco  5384  fcoconst  5388  fcof1  5476  isotr  5509  isopolem  5514  f1oiso  5518  acexmidlemcase  5560  ovprc1  5594  fnoprabg  5655  op1steq  5858  1stconst  5895  f1o2ndf1  5902  sprmpt2  5913  brtpos2  5922  tpostpos  5935  tposf12  5940  smores  5963  tfrlemi1  6003  tfr1onlembfn  6015  tfri1dALT  6022  tfrcllembfn  6028  freceq1  6063  freceq2  6064  frectfr  6071  omv2  6131  omsuc  6138  nnsucelsuc  6157  nntri3  6163  nnaordi  6170  nnmordi  6178  nnm00  6191  ecexr  6200  ertr  6210  swoer  6223  erth  6239  ecelqsdm  6265  iinerm  6267  ecinxp  6270  erovlem  6287  dom3  6346  phpelm  6424  nnwetri  6462  supubti  6508  supisoex  6518  ordiso2  6542  djuun  6569  en2eleq  6598  en2other2  6599  dmaddpqlem  6706  distrnqg  6716  ltanqi  6731  ltmnqi  6732  ltaddnq  6736  ltrnqg  6749  ltnnnq  6752  enq0sym  6761  addnq0mo  6776  mulnq0mo  6777  addnnnq0  6778  distrnq0  6788  prarloclemn  6828  prarloc  6832  ltdfpr  6835  genplt2i  6839  addnqprl  6858  addnqpru  6859  nqprl  6880  appdivnq  6892  1idprl  6919  1idpru  6920  ltexpri  6942  recexpr  6967  cauappcvgprlemdisj  6980  archrecpr  6993  addsrmo  7059  mulsrmo  7060  addsrpr  7061  mulsrpr  7062  0idsr  7083  1idsr  7084  archsr  7097  prsradd  7101  prsrlt  7102  caucvgsr  7117  elrealeu  7137  muladd11r  7408  negeu  7443  pncan  7458  pncan3  7460  negsub  7500  addid0  7621  posdif  7703  ltnegcon1  7711  subge0  7723  suble0  7724  lesub0  7727  reapval  7820  reapneg  7841  ap0gt0  7882  recextlem1  7885  div0ap  7934  recrecap  7941  rec11ap  7942  recgt0  8072  mulgt1  8085  lerec2  8111  recp1lt1  8121  recreclt  8122  ledivp1  8125  negiso  8177  nnsub  8221  avglt1  8413  nnrecl  8430  nnnn0addcl  8462  elnn0nn  8474  nn0ge2m1nn  8492  zaddcl  8549  eluzadd  8805  divfnzn  8864  qaddcl  8878  qreccl  8885  cnref1o  8891  ge0p1rp  8923  divlt1lt  8959  divle1le  8960  addlelt  8997  xrre3  9042  xltnegi  9055  ixxssixx  9078  iccshftr  9169  iccshftl  9171  iccdil  9173  icccntr  9175  zltaddlt1le  9181  elfz2  9189  peano2fzr  9209  fzdcel  9212  fzsplit2  9222  fzaddel  9230  fzrev2  9255  fzrev2i  9256  fzrev3  9257  elfz1b  9260  fseq1p1m1  9264  uzsubfz0  9294  fzosubel3  9359  eluzgtdifelfzo  9360  fzofzp1b  9391  elfzomelpfzo  9394  exfzdc  9403  fvinim0ffz  9404  exbtwnzlemshrink  9412  qbtwnz  9415  qbtwnxr  9421  ico0  9425  apbtwnz  9433  flqge  9441  flqlt  9442  flqltnz  9446  flqbi2  9450  flqaddz  9456  flqmulnn0  9458  intfracq  9479  flqdiv  9480  q0mod  9514  q1mod  9515  mulp1mod1  9524  q2txmodxeq0  9543  modfzo0difsn  9554  frec2uzuzd  9561  frec2uzltd  9562  frec2uzrand  9564  iseqsplit  9631  iseqcaopr  9635  expivallem  9651  expival  9652  expinnval  9653  exp1  9656  expcl2lemap  9662  rpexpcl  9669  expnegzap  9684  mulexp  9689  mulexpzap  9690  leexp2r  9704  leexp1a  9705  sq11  9722  subsq  9755  binom2  9759  binom3  9764  zesq  9765  bernneq  9767  sq11ap  9813  facwordi  9841  facubnd  9846  facavg  9847  bcval  9850  ibcval5  9864  hashennn  9881  fihashf1rn  9890  fseq1hash  9902  hashdifsn  9920  hashdifpr  9921  hashxp  9927  shftfvalg  9932  ovshftex  9933  shftdm  9936  shftfib  9937  shftval  9939  shftf  9944  crre  9970  cjexp  10006  cjreim2  10017  uzin2  10099  rexuz3  10102  resqrexlemgt0  10132  resqrex  10138  sqrtgt0  10146  sqrtsq  10156  sqrtmsq  10157  absrpclap  10173  absext  10175  absmul  10181  absid  10183  absexp  10191  nn0abscl  10197  abslt  10200  absle  10201  recvalap  10209  abstri  10216  caubnd2  10229  qdenre  10314  maxabsle  10316  maxabslemval  10320  maxcl  10322  rexanre  10332  min1inf  10339  climconst2  10356  climmpt  10365  climres  10368  climcaucn  10414  sumeq1  10418  dvdsdc  10436  iddvdsexp  10452  dvdsadd  10471  dvds1  10486  odd2np1  10505  oddm1even  10507  m1exp1  10533  divalglemnn  10550  fldivndvdslt  10567  flodddiv4lt  10568  zsupcllemex  10574  infssuzcldc  10579  dvdsbnd  10580  gcdnncl  10591  zeqzmulgcd  10594  gcdneg  10605  modgcd  10614  bezoutlemex  10622  bezoutlemeu  10628  dfgcd3  10631  gcdzeq  10643  dvdssq  10652  eucalgval2  10667  eucialgcvga  10672  lcmval  10677  gcddvdslcm  10687  lcmneg  10688  coprmgcdb  10702  qredeu  10711  divgcdcoprm0  10715  divgcdcoprmex  10716  cncongr1  10717  cncongr2  10718  cncongrcoprm  10720  prmind2  10734  dvdsnprmd  10739  exprmfct  10751  isprm6  10758  pw2dvdslemn  10775  oddpwdclemdc  10783  sqrt2irraplemnn  10789  divnumden  10806  divdenle  10807  nn0sqrtelqelz  10816  phivalfi  10820  crth  10832  xpct  10841  znnen  10843  bj-indind  11019  bj-omtrans  11043  bj-inf2vnlem1  11057  sscoll2  11075  qdencn  11077
  Copyright terms: Public domain W3C validator