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

Theorem imp 122
Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
imp.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imp ((𝜑𝜓) → 𝜒)

Proof of Theorem imp
StepHypRef Expression
1 simpl 107 . 2 ((𝜑𝜓) → 𝜑)
2 simpr 108 . 2 ((𝜑𝜓) → 𝜓)
3 imp.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3sylc 61 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  impcom  123  impd  251  imp31  252  imp32  253  expdimp  255  impancom  256  pm3.22  261  ancoms  264  adantr  270  impel  274  biimpa  290  biimpar  291  biimpac  292  biimparc  293  pm3.33  337  pm3.34  338  pm3.35  339  pm5.31  340  imp4b  342  imp41  345  imp42  346  imp43  347  imp44  348  imp45  349  imp5g  352  expr  367  impac  373  sylan9  401  sylan9r  402  imdistani  434  mpan10  458  anabsi5  544  anim12dan  565  pm3.43  567  con3dimp  597  imnan  657  jaoian  742  jaodan  744  impidc  791  pm2.5dc  799  con2bidc  805  pm5.18dc  813  dfandc  814  pm4.63dc  816  annimim  818  pm4.54dc  841  pm4.79dc  845  orcanai  873  annimdc  881  pm4.55dc  882  orandc  883  pm4.82  894  pm3.11dc  901  pm3.12dc  902  dn1dc  904  3jcad  1122  3expia  1143  3an1rs  1153  3imp1  1154  3imp2  1156  syl3anl2  1221  3jaoian  1239  3jaodan  1240  mp3anl1  1265  mp3anl2  1266  mp3anl3  1267  ecased  1283  xor3dc  1321  pm5.15dc  1323  xor2dc  1324  xornbidc  1325  xordc  1326  nbbndc  1328  biassdc  1329  bilukdc  1330  dfbi3dc  1331  pm5.24dc  1332  xordidc  1333  alanimi  1391  19.29  1554  equs4  1657  equsexd  1661  spimth  1667  equs5a  1719  ax11v2  1745  ax11b  1751  equs5or  1755  sb5rf  1777  equvin  1788  nfsb4t  1935  eu5  1992  mopick  2023  euexex  2030  2euswapdc  2036  exists2  2042  eqrdav  2084  dvelimdc  2244  nebidc  2331  pm13.18  2332  nelne1  2341  nelne2  2342  ralrimdvv  2453  r19.21bi  2457  r19.26  2493  ralbi  2497  rexbi  2498  r19.29  2502  vtoclgft  2663  rspcva  2713  rspc2va  2727  elabgt  2748  eqeu  2776  mob2  2786  mob  2788  euind  2793  reu6  2795  reuind  2809  sbctt  2894  rspsbca  2911  sbcnestgf  2968  rspcsbela  2976  ssel2  3009  sselda  3014  sstr  3022  nssne1  3071  nssne2  3072  reuss2  3268  reupick  3272  reupick2  3274  reximdva0m  3287  ssn0  3313  disjel  3325  ssdisj  3327  absneu  3497  preqr1g  3593  prel12  3598  dfiun2g  3745  nbrne1  3837  nbrne2  3838  mpteq12f  3893  triun  3924  csbexga  3942  iinexgm  3965  prexg  4012  copsex2t  4046  swopo  4107  poirr  4108  potr  4109  pofun  4113  issod  4120  ordelss  4180  trssord  4181  limelon  4200  trsuc  4223  eusvnfb  4250  rabxfrd  4265  regexmidlem1  4322  nordeq  4333  suc11g  4346  nnsuc  4403  brrelex12  4447  vtoclr  4454  optocl  4482  relop  4554  brcogw  4573  breldmg  4610  elreldm  4629  riinint  4662  issref  4781  xpidtr  4789  trin2  4790  cnveqb  4852  funopg  5013  funssres  5021  fununi  5047  funimass2  5057  imain  5061  fnun  5085  fco  5140  opelf  5146  f0rn0  5168  f1oun  5236  fun11iun  5237  fv3  5291  ndmfvg  5298  fvelima  5319  fvopab3ig  5341  fvmptssdm  5350  fvmptf  5358  fvimacnv  5377  fmptco  5427  funfvima2  5488  funfvima3  5489  f1veqaeq  5509  f1ocnvfvrneq  5522  fliftfun  5536  isotr  5556  isoini  5558  isopolem  5562  isosolem  5564  moriotass  5597  acexmidlem2  5610  suppssfv  5809  suppssov1  5810  f1dmex  5844  releldm2  5912  f1o2ndf1  5950  poxp  5954  tposf2  5987  iunon  6003  smoel2  6022  tfrlem9  6038  tfrexlem  6053  tfr1onlembxssdm  6062  tfr1onlemres  6068  tfrcllembxssdm  6075  tfrcllemres  6081  tfrcl  6083  tfri3  6086  frecabcl  6118  sucinc2  6161  nnacom  6199  nnmcom  6204  nnsucsssuc  6207  nnsucuniel  6210  nntri2or2  6213  nnaordi  6219  nnmordi  6227  nnaordex  6238  nnm00  6240  ectocld  6310  iinerm  6316  th3qlem2  6347  elpm2r  6375  mapsncnv  6404  f1oen3g  6423  f1oeng  6426  en2d  6437  en3d  6438  dom2lem  6441  fundmen  6475  fundmeng  6476  unen  6485  xpdom2  6499  xpdom2g  6500  fopwdom  6504  nneneq  6525  phpm  6533  phpelm  6534  dif1enen  6548  fin0  6553  findcard  6556  diffifi  6562  ac6sfi  6566  onunsnss  6579  xpfi  6590  sbthlem1  6610  sbthlemi3  6612  sbthlemi10  6619  isotilem  6645  inflbti  6663  ordiso2  6672  eldju2ndl  6707  eldju2ndr  6708  updjudhf  6714  carden2bex  6761  pm54.43  6762  exmidfodomrlemeldju  6769  exmidfodomrlemreseldju  6770  exmidfodomrlemim  6771  ltmpig  6842  enq0sym  6935  addnq0mo  6950  mulnq0mo  6951  prarloclem3step  6999  prarloclem3  7000  genpml  7020  genpmu  7021  genprndl  7024  genprndu  7025  genpdisj  7026  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  distrlem5prl  7089  distrlem5pru  7090  ltsopr  7099  ltaddpr  7100  addcanprleml  7117  addcanprlemu  7118  recexprlemm  7127  recexprlemlol  7129  recexprlemupu  7131  aptiprleml  7142  aptiprlemu  7143  caucvgprlemnkj  7169  caucvgprlemnbj  7170  addsrmo  7233  mulsrmo  7234  srpospr  7272  caucvgsr  7291  axprecex  7359  mulgt0  7504  ltne  7514  cnegexlem1  7601  cnegexlem2  7602  negf1o  7804  addgt0  7870  addgegt0  7871  addgtge0  7872  addge0  7873  recexre  7996  mulge0  8037  recexap  8061  prodgt02  8249  prodge02  8251  ltmul12a  8256  mulgt1  8259  nndivtr  8398  addltmul  8585  elnnnn0b  8650  xnn0nnn0pnf  8682  elnnz  8693  zmulcl  8736  nn0n0n1ge2  8750  nn0lt2  8761  uzind2  8791  nn0ind-raph  8796  eluzp1m1  8974  uz3m2nn  8993  supinfneg  9015  infsupneg  9016  negm  9032  lbzbi  9033  qaddcl  9052  qmulcl  9054  qreccl  9059  ledivge1le  9135  nn0ledivnn  9170  xrltne  9210  xrre  9214  xrre2  9215  xrre3  9216  ge0gtmnf  9217  xltnegi  9229  iccsupr  9316  icoshft  9339  icoshftf1o  9340  fznlem  9387  fzen  9389  uzsubsubfz  9393  fzsuc2  9423  elfz1b  9434  elfz0ubfz0  9464  elfz0fzfz0  9465  fz0fzelfz0  9466  fz0fzdiffz0  9469  elfzmlbp  9471  difelfznle  9474  fzofzim  9527  eluzgtdifelfzo  9536  elfzodifsumelfzo  9540  elfzonlteqm1  9549  elfzom1p1elfzo  9553  ssfzo12bi  9564  subfzo0  9581  exbtwnzlemstep  9587  modqmuladdnn0  9703  modfzo0difsn  9730  addmodlteq  9733  frec2uzlt2d  9739  frecuzrdgtcl  9747  frecuzrdgfunlem  9754  iseqid3  9840  m1expcl2  9875  expge1  9890  leexp2r  9907  expubnd  9910  zesq  9968  expnlbnd  9974  nn0opthd  10026  faclbnd  10045  bcpasc  10070  hashprg  10112  iseqcoll  10143  rexanuz  10316  rexuz3  10318  r19.29uz  10320  r19.2uz  10321  absnid  10401  leabs  10402  ltabs  10415  icodiamlt  10508  maxleast  10541  negfi  10552  climcn2  10590  climcau  10626  climcaucn  10630  sumdc  10637  fisumcvg  10656  isumz  10667  fsumf1o  10668  fisumss  10670  dvds0lem  10681  dvds2ln  10704  dvdssub2  10713  dvdsadd2b  10718  dvdsabseq  10723  divconjdvds  10725  dvdsdivcl  10726  odd2np1  10748  oddge22np1  10756  opoe  10770  omoe  10771  opeo  10772  omeo  10773  m1expo  10775  nn0ehalf  10778  nn0o1gt2  10780  nno  10781  divalgb  10800  ndvdsadd  10806  zsupcllemex  10817  zssinfcl  10819  gcd0id  10845  gcdneg  10848  gcdaddm  10850  bezoutlemstep  10861  dfgcd2  10878  gcddiv  10883  dvdsmulgcd  10889  bezoutr  10896  bezoutr1  10897  ialgfx  10909  lcmgcdlem  10934  lcmgcdeq  10940  coprmdvds  10949  divgcdcoprmex  10959  cncongr1  10960  cncongr2  10961  isprm3  10975  dvdsnprmd  10982  prmgt1  10988  oddprmgt2  10990  isprm6  11001  cncongrprm  11011  phibndlem  11067  phimullem  11076  bj-prexg  11240  peano5set  11273  bj-peano4  11288  bj-nn0suc  11297  bj-nn0sucALT  11311  bj-findis  11312  exmidsbthrlem  11350
  Copyright terms: Public domain W3C validator