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

Theorem simpl 108
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 ((𝜑𝜓) → 𝜑)

Proof of Theorem simpl
StepHypRef Expression
1 ax-ia1 105 1 ((𝜑𝜓) → 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-ia1 105
This theorem is referenced by:  simpli  110  simpld  111  imp  123  adantrd  277  iba  298  pm3.41  329  pm4.45im  332  anim12  341  pm4.71  386  adantlr  468  adantrr  470  adantllr  472  adantlrr  474  adantrlr  476  adantrrr  478  simplll  522  simplrl  524  simprll  526  simprrl  528  anabs1  561  jcab  592  pm4.38  594  pm5.21  684  ioran  741  pm3.14  742  pm4.44  768  ordi  805  pm4.39  811  pm5.16  813  pm5.54dc  903  intnanr  915  intnanrd  917  dcan  918  dedlema  953  dedlemb  954  pm4.42r  955  prlem2  958  simp1l  1005  simp2l  1007  simp3l  1009  3anandis  1325  xordc1  1371  anxordi  1378  falantru  1381  19.26  1457  exsimpl  1596  sbequ2  1742  sbcof2  1782  sbequilem  1810  sbequ8  1819  euan  2055  mooran1  2071  eupickbi  2081  2exeu  2091  dimatis  2116  rexim  2526  r19.26  2558  r19.40  2585  rspcime  2796  rr19.28v  2824  elrab3t  2839  eueq3dc  2858  mosubt  2861  reu6  2873  sbc2iegf  2979  sbcralt  2985  sbcrext  2986  rmob  3001  csbiebt  3039  ssab2  3181  difdif  3201  uneqin  3327  indifdir  3332  undif3ss  3337  rexm  3462  eqifdc  3506  ifandc  3508  difsn  3660  opprc1  3730  unissel  3768  ssmin  3793  abssexg  4109  undifexmid  4120  pwntru  4125  exmidundif  4132  exmidundifim  4133  opelopabsb  4185  sess1  4262  ordelord  4306  onin  4311  suctr  4346  abnexg  4370  ordtriexmidlem  4438  ordtri2or2exmid  4489  tfi  4499  peano1  4511  peano2  4512  nnpredcl  4539  0nelxp  4570  0nelelxp  4571  brab2a  4595  mosubopt  4607  posng  4614  opabssxp  4616  ideqg  4693  relssres  4860  trin2  4933  dminss  4956  iota4an  5110  iota2  5117  fun11uni  5196  imadiflem  5205  funimaexg  5210  fneq12  5219  fvelrnb  5472  dffo4  5571  ffnfv  5581  ffvresb  5586  fmptco  5589  fcoconst  5594  fcof1  5687  isotr  5720  isopolem  5726  f1oiso  5730  acexmidlemcase  5772  ovprc1  5810  fnoprabg  5875  op1steq  6080  dmmpog  6110  1stconst  6121  f1o2ndf1  6128  brtpos2  6151  tpostpos  6164  tposf12  6169  smores  6192  tfrlemi1  6232  tfr1onlembfn  6244  tfri1dALT  6251  tfrcllembfn  6257  freceq1  6292  freceq2  6293  frectfr  6300  omv2  6364  omsuc  6371  nnsucelsuc  6390  nntri3  6396  nnaordi  6407  nnmordi  6415  nnm00  6428  ecexr  6437  ertr  6447  swoer  6460  erth  6476  ecelqsdm  6502  iinerm  6504  ecinxp  6507  erovlem  6524  pmresg  6573  resixp  6630  elixpsn  6632  mapsnf1o  6634  dom3  6673  mapdom1g  6744  ssenen  6748  phpelm  6763  finexdc  6799  nnwetri  6807  fiintim  6820  ssfii  6865  fiss  6868  supubti  6889  supisoex  6899  ordiso2  6923  inl11  6953  omp1eomlem  6982  nnnninf  7026  ctssexmid  7027  ismkvnex  7032  omniwomnimkv  7044  en2eleq  7063  en2other2  7064  exmidfodomrlemr  7070  exmidfodomrlemrALT  7071  exmidaclem  7076  djuen  7079  djudoml  7087  cc1  7092  dmaddpqlem  7204  distrnqg  7214  ltanqi  7229  ltmnqi  7230  ltaddnq  7234  ltrnqg  7247  ltnnnq  7250  enq0sym  7259  addnq0mo  7274  mulnq0mo  7275  addnnnq0  7276  distrnq0  7286  prarloclemn  7326  prarloc  7330  ltdfpr  7333  genplt2i  7337  addnqprl  7356  addnqpru  7357  nqprl  7378  appdivnq  7390  1idprl  7417  1idpru  7418  ltexpri  7440  recexpr  7465  cauappcvgprlemdisj  7478  archrecpr  7491  addsrmo  7570  mulsrmo  7571  addsrpr  7572  mulsrpr  7573  0idsr  7594  1idsr  7595  archsr  7609  prsradd  7613  prsrlt  7614  caucvgsr  7629  map2psrprg  7632  elrealeu  7656  muladd11r  7937  negeu  7972  pncan  7987  pncan3  7989  negsub  8029  addid0  8154  posdif  8236  ltnegcon1  8244  subge0  8256  suble0  8257  lesub0  8260  reapval  8357  reapneg  8378  ap0gt0  8421  aprcl  8427  lt0ap0  8429  recextlem1  8431  div0ap  8481  recrecap  8488  rec11ap  8489  recgt0  8627  mulgt1  8640  lerec2  8666  recp1lt1  8676  recreclt  8677  ledivp1  8680  negiso  8732  nnsub  8778  avglt1  8977  nnrecl  8994  nnnn0addcl  9026  elnn0nn  9038  nn0ge2m1nn  9056  zaddcl  9113  eluzadd  9373  divfnzn  9435  qaddcl  9449  qreccl  9456  cnref1o  9462  ge0p1rp  9495  divlt1lt  9534  divle1le  9535  addlelt  9578  xrre3  9628  xltnegi  9641  xaddval  9651  xaddcom  9667  xnegdi  9674  xposdif  9688  ixxssixx  9708  iccshftr  9800  iccshftl  9802  iccdil  9804  icccntr  9806  zltaddlt1le  9813  elfz2  9821  peano2fzr  9841  fzdcel  9844  fzsplit2  9854  fzaddel  9863  fzrev2  9889  fzrev2i  9890  fzrev3  9891  elfz1b  9894  fseq1p1m1  9898  uzsubfz0  9930  fzosubel3  9997  eluzgtdifelfzo  9998  fzofzp1b  10029  elfzomelpfzo  10032  exfzdc  10041  fvinim0ffz  10042  exbtwnzlemshrink  10050  qbtwnz  10053  qbtwnxr  10059  ico0  10063  apbtwnz  10071  flqge  10079  flqlt  10080  flqltnz  10084  flqbi2  10088  flqaddz  10094  flqmulnn0  10096  intfracq  10117  flqdiv  10118  q0mod  10152  q1mod  10153  mulp1mod1  10162  q2txmodxeq0  10181  modfzo0difsn  10192  frec2uzuzd  10199  frec2uzltd  10200  frec2uzrand  10202  uzennn  10233  seq3split  10276  seq3caopr  10280  exp3vallem  10318  exp3val  10319  expnnval  10320  exp1  10323  expcl2lemap  10329  rpexpcl  10336  expnegzap  10351  mulexp  10356  mulexpzap  10357  leexp2r  10371  leexp1a  10372  sq11  10389  subsq  10423  binom2  10427  binom3  10433  zesq  10434  bernneq  10436  sq11ap  10482  facwordi  10510  facubnd  10515  facavg  10516  bcval  10519  bcval5  10533  hashennn  10550  fihashf1rn  10559  fseq1hash  10571  hashdifsn  10589  hashdifpr  10590  hashxp  10596  fnfz0hash  10599  ffzo0hash  10601  shftfvalg  10614  ovshftex  10615  shftdm  10618  shftfib  10619  shftval  10621  shftf  10626  crre  10653  cjexp  10689  cjreim2  10700  uzin2  10783  rexuz3  10786  resqrexlemgt0  10816  resqrex  10822  sqrtgt0  10830  sqrtsq  10840  sqrtmsq  10841  absrpclap  10857  absext  10859  absmul  10865  absid  10867  absexp  10875  nn0abscl  10881  abslt  10884  absle  10885  recvalap  10893  abstri  10900  caubnd2  10913  qdenre  10998  maxabsle  11000  maxabslemval  11004  maxcl  11006  rexanre  11016  min1inf  11027  minabs  11031  minclpr  11032  mul0inf  11036  xrmaxiflemcl  11038  xrnegiso  11055  climconst2  11084  climmpt  11093  climres  11096  climcaucn  11144  sumeq1  11148  summodclem2a  11174  isumz  11182  fisumss  11185  fsumzcl2  11198  sumsnf  11202  isumclim3  11216  fsum2dlemstep  11227  fisumcom2  11231  fsumconst  11247  cvgcmpub  11269  binom  11277  binom1p  11278  binom1dif  11280  bcxmas  11282  divcnv  11290  geo2lim  11309  geoisum  11310  geoisumr  11311  geoisum1  11312  mertenslemi1  11328  mertensabs  11330  efcllem  11389  efcj  11403  efadd  11405  efexp  11412  efgt1p2  11425  tanvalap  11438  tanval2ap  11443  tanval3ap  11444  sinadd  11466  cosadd  11467  dvdsdc  11524  iddvdsexp  11540  dvdsadd  11559  dvds1  11574  odd2np1  11593  oddm1even  11595  m1exp1  11621  divalglemnn  11638  fldivndvdslt  11655  flodddiv4lt  11656  zsupcllemex  11662  infssuzcldc  11667  dvdsbnd  11668  gcdnncl  11679  zeqzmulgcd  11682  gcdneg  11693  modgcd  11702  bezoutlemex  11712  bezoutlemeu  11718  dfgcd3  11721  gcdzeq  11733  dvdssq  11742  algrf  11749  eucalgval2  11757  eucalgcvga  11762  lcmval  11767  gcddvdslcm  11777  lcmneg  11778  coprmgcdb  11792  qredeu  11801  divgcdcoprm0  11805  divgcdcoprmex  11806  cncongr1  11807  cncongr2  11808  cncongrcoprm  11810  prmind2  11824  dvdsnprmd  11829  exprmfct  11841  isprm6  11848  pw2dvdslemn  11866  oddpwdclemdc  11874  sqrt2irraplemnn  11880  divnumden  11897  divdenle  11898  nn0sqrtelqelz  11907  phivalfi  11911  crth  11923  xpct  11932  znnen  11934  ennnfonelemg  11939  ennnfone  11961  ctinfom  11964  ctinf  11966  isstruct2im  11995  isstruct2r  11996  setsvalg  12015  setsslnid  12036  ressid2  12044  ressval2  12045  2strbasg  12086  2stropg  12087  2strbas1g  12089  restval  12152  restid2  12155  eltg2b  12249  difopn  12303  ntrcls0  12326  neii1  12342  restbasg  12363  resttopon  12366  restuni2  12372  cnrest2r  12432  tx1cn  12464  txcnp  12466  txcn  12470  txswaphmeo  12516  psmettri  12525  xmeteq0  12554  xmettri  12567  metrtri  12572  ssblex  12626  xmeter  12631  isxms2  12647  cnbl0  12729  cnblcld  12730  reopnap  12733  tgioo  12741  addcncntoplem  12746  rescncf  12763  cncffvrn  12764  mulc1cncf  12771  cncfcncntop  12775  addccncf  12781  cdivcncfap  12782  negcncf  12783  cnopnap  12789  suplociccex  12798  limccl  12823  ellimc3apf  12824  cnplimcim  12831  limccnp2lem  12840  reldvg  12843  dvbsssg  12850  dvcjbr  12867  dvcj  12868  dvfre  12869  dvrecap  12872  dvef  12883  reeff1olem  12887  pilem3  12898  ptolemy  12939  rplogcl  12994  rpcxpef  13009  cxprec  13025  rpcxproot  13028  rplogb1  13058  logbgt0b  13076  bj-nnan  13092  bj-indind  13274  bj-omtrans  13298  bj-inf2vnlem1  13312  sscoll2  13330  pwtrufal  13338  sssneq  13343  pw1nct  13344  nninfsellemsuc  13356  nninfomnilem  13362  exmidsbthrlem  13365  qdencn  13370  trilpo  13384  trirec0  13385  apdiff  13389  iswomninnlem  13390  redcwlpo  13395  dcapncf  13396  neapmkv  13398
  Copyright terms: Public domain W3C validator