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

Theorem imp 123
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 108 . 2 ((𝜑𝜓) → 𝜑)
2 simpr 109 . 2 ((𝜑𝜓) → 𝜓)
3 imp.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3sylc 62 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  impcom  124  impd  252  imp31  254  imp32  255  expdimp  257  impancom  258  pm3.22  263  ancoms  266  adantr  272  impel  276  biimpa  292  biimpar  293  biimpac  294  biimparc  295  pm3.33  340  pm3.34  341  pm3.35  342  pm5.31  343  imp4b  345  imp41  348  imp42  349  imp43  350  imp44  351  imp45  352  imp5g  355  expr  370  impac  376  sylan9  404  sylan9r  405  imdistani  439  mpan10  463  a2and  530  anabsi5  551  anim12dan  572  pm3.43  574  con3dimp  607  annimim  658  imnan  662  jaoian  767  jaodan  769  stdcndc  813  impidc  826  pm2.5gdc  834  con2bidc  843  pm5.18dc  851  dfandc  852  pm4.63dc  854  pm4.54dc  870  pm4.79dc  871  orcanai  896  annimdc  904  pm4.55dc  905  orandc  906  pm4.82  917  pm3.11dc  924  pm3.12dc  925  dn1dc  927  3jcad  1145  3expia  1166  3an1rs  1180  3imp1  1181  3imp2  1183  syl3anl2  1248  3jaoian  1266  3jaodan  1267  mp3anl1  1292  mp3anl2  1293  mp3anl3  1294  ecased  1310  xor3dc  1348  pm5.15dc  1350  xor2dc  1351  xornbidc  1352  xordc  1353  nbbndc  1355  biassdc  1356  bilukdc  1357  dfbi3dc  1358  pm5.24dc  1359  xordidc  1360  alanimi  1418  19.29  1582  equs4  1686  equsexd  1690  spimth  1696  equs5a  1748  ax11v2  1774  ax11b  1780  equs5or  1784  sb5rf  1806  equvin  1817  nfsb4t  1965  eu5  2022  mopick  2053  euexex  2060  2euswapdc  2066  exists2  2072  eqrdav  2114  dvelimdc  2276  nebidc  2363  pm13.18  2364  nelne1  2373  nelne2  2374  ralrimdvv  2491  r19.21bi  2495  r19.26  2533  ralbi  2539  rexbi  2540  r19.29  2544  vtoclgft  2708  rspcva  2759  rspc2va  2775  elabgt  2797  eqeu  2825  mob2  2835  mob  2837  euind  2842  reu6  2844  reuind  2860  sbctt  2945  rspsbca  2962  sbcnestgf  3019  rspcsbela  3027  ssel2  3060  sselda  3065  sstr  3073  nssne1  3123  nssne2  3124  reuss2  3324  reupick  3328  reupick2  3330  reximdva0m  3346  ssn0  3373  disjel  3385  ssdisj  3387  absneu  3563  preqr1g  3661  prel12  3666  dfiun2g  3813  nbrne1  3915  nbrne2  3916  mpteq12f  3976  triun  4007  csbexga  4024  iinexgm  4047  prexg  4101  copsex2t  4135  swopo  4196  poirr  4197  potr  4198  pofun  4202  issod  4209  ordelss  4269  trssord  4270  limelon  4289  trsuc  4312  eusvnfb  4343  rabxfrd  4358  regexmidlem1  4416  nordeq  4427  suc11g  4440  nnsuc  4497  brrelex12  4545  vtoclr  4555  optocl  4583  relop  4657  brcogw  4676  breldmg  4713  elreldm  4733  riinint  4768  issref  4889  xpidtr  4897  trin2  4898  cnveqb  4962  funopg  5125  funssres  5133  fununi  5159  funimass2  5169  imain  5173  fnun  5197  fco  5256  opelf  5262  f0rn0  5285  f1oun  5353  fun11iun  5354  fv3  5410  ndmfvg  5418  fvelima  5439  fvopab3ig  5461  fvmptssdm  5471  fvmptf  5479  fvimacnv  5501  fmptco  5552  funfvima2  5616  funfvima3  5617  f1veqaeq  5636  f1ocnvfvrneq  5649  fliftfun  5663  isotr  5683  isoini  5685  isopolem  5689  isosolem  5691  moriotass  5724  acexmidlem2  5737  suppssfv  5944  suppssov1  5945  f1dmex  5980  releldm2  6049  f1o2ndf1  6091  poxp  6095  tposf2  6131  iunon  6147  smoel2  6166  tfrlem9  6182  tfrexlem  6197  tfr1onlembxssdm  6206  tfr1onlemres  6212  tfrcllembxssdm  6219  tfrcllemres  6225  tfrcl  6227  tfri3  6230  frecabcl  6262  sucinc2  6308  nnacom  6346  nnmcom  6351  nnsucsssuc  6354  nnsucuniel  6357  nntri2or2  6360  nnaordi  6370  nnmordi  6378  nnaordex  6389  nnm00  6391  ectocld  6461  iinerm  6467  th3qlem2  6498  elpm2r  6526  mapsncnv  6555  mptelixpg  6594  ixpsnf1o  6596  f1oen3g  6614  f1oeng  6617  en2d  6628  en3d  6629  dom2lem  6632  fundmen  6666  fundmeng  6667  unen  6676  xpdom2  6691  xpdom2g  6692  fopwdom  6696  nneneq  6717  phpm  6725  phpelm  6726  dif1enen  6740  fin0  6745  findcard  6748  diffifi  6754  ac6sfi  6758  onunsnss  6771  fiintim  6783  xpfi  6784  fidcenum  6810  sbthlem1  6811  sbthlemi3  6813  sbthlemi10  6820  elfir  6827  isotilem  6859  inflbti  6877  ordiso2  6886  eldju2ndl  6923  eldju2ndr  6924  updjudhf  6930  mkvprop  6998  carden2bex  7011  pm54.43  7012  exmidfodomrlemeldju  7019  exmidfodomrlemreseldju  7020  exmidfodomrlemim  7021  ltmpig  7111  enq0sym  7204  addnq0mo  7219  mulnq0mo  7220  prarloclem3step  7268  prarloclem3  7269  genpml  7289  genpmu  7290  genprndl  7293  genprndu  7294  genpdisj  7295  distrlem1prl  7354  distrlem1pru  7355  distrlem4prl  7356  distrlem4pru  7357  distrlem5prl  7358  distrlem5pru  7359  ltsopr  7368  ltaddpr  7369  addcanprleml  7386  addcanprlemu  7387  recexprlemm  7396  recexprlemlol  7398  recexprlemupu  7400  aptiprleml  7411  aptiprlemu  7412  caucvgprlemnkj  7438  caucvgprlemnbj  7439  addsrmo  7515  mulsrmo  7516  srpospr  7555  caucvgsr  7574  axprecex  7652  mulgt0  7803  ltne  7813  cnegexlem1  7901  cnegexlem2  7902  negf1o  8108  addgt0  8174  addgegt0  8175  addgtge0  8176  addge0  8177  recexre  8303  mulge0  8344  recexap  8374  prodgt02  8568  prodge02  8570  ltmul12a  8575  mulgt1  8578  nndivtr  8719  addltmul  8907  elnnnn0b  8972  xnn0nnn0pnf  9004  elnnz  9015  zmulcl  9058  nn0n0n1ge2  9072  nn0lt2  9083  nn0le2is012  9084  uzind2  9114  nn0ind-raph  9119  eluzp1m1  9298  uz3m2nn  9317  supinfneg  9339  infsupneg  9340  negm  9356  lbzbi  9357  qaddcl  9376  qmulcl  9378  qreccl  9383  ledivge1le  9459  nn0ledivnn  9494  xrltne  9536  xrre  9543  xrre2  9544  xrre3  9545  ge0gtmnf  9546  xltnegi  9558  xnn0xadd0  9590  xnegdi  9591  xposdif  9605  xlesubadd  9606  iccsupr  9689  icoshft  9713  icoshftf1o  9714  fznlem  9761  fzen  9763  uzsubsubfz  9767  fzsuc2  9799  elfz1b  9810  elfz0ubfz0  9842  elfz0fzfz0  9843  fz0fzelfz0  9844  fz0fzdiffz0  9847  elfzmlbp  9849  difelfznle  9852  fzofzim  9905  eluzgtdifelfzo  9914  elfzodifsumelfzo  9918  elfzonlteqm1  9927  elfzom1p1elfzo  9931  ssfzo12bi  9942  subfzo0  9959  exbtwnzlemstep  9965  modqmuladdnn0  10081  modfzo0difsn  10108  addmodlteq  10111  frec2uzlt2d  10117  frecuzrdgtcl  10125  frecuzrdgfunlem  10132  m1expcl2  10255  expge1  10270  leexp2r  10287  expubnd  10290  zesq  10350  expnlbnd  10356  nn0opthd  10408  faclbnd  10427  bcpasc  10452  hashprg  10494  seq3coll  10525  rexanuz  10700  rexuz3  10702  r19.29uz  10704  r19.2uz  10705  absnid  10785  leabs  10786  ltabs  10799  icodiamlt  10892  maxleast  10925  negfi  10939  climcn2  11018  climcau  11056  climcaucn  11060  sumdc  11067  fsum3cvg  11086  isumz  11098  fsumf1o  11099  fisumss  11101  isumss2  11102  fsumzcl2  11114  fsumsplit  11116  fsumsplitsnun  11128  sumsplitdc  11141  fsum2dlemstep  11143  telfsumo  11175  fsumparts  11179  fsumiun  11186  isumrpcl  11203  efexp  11287  efieq1re  11376  dvds0lem  11399  dvds2ln  11422  dvdssub2  11431  dvdsadd2b  11436  dvdsabseq  11441  divconjdvds  11443  dvdsdivcl  11444  odd2np1  11466  oddge22np1  11474  opoe  11488  omoe  11489  opeo  11490  omeo  11491  m1expo  11493  nn0ehalf  11496  nn0o1gt2  11498  nno  11499  divalgb  11518  ndvdsadd  11524  zsupcllemex  11535  zssinfcl  11537  gcd0id  11563  gcdneg  11566  gcdaddm  11568  bezoutlemstep  11581  dfgcd2  11598  gcddiv  11603  dvdsmulgcd  11609  bezoutr  11616  bezoutr1  11617  algfx  11629  lcmgcdlem  11654  lcmgcdeq  11660  coprmdvds  11669  divgcdcoprmex  11679  cncongr1  11680  cncongr2  11681  isprm3  11695  dvdsnprmd  11702  prmgt1  11708  oddprmgt2  11710  isprm6  11721  cncongrprm  11731  phibndlem  11787  phimullem  11796  ennnfone  11833  unct  11849  uniopn  12063  istopon  12075  fiinbas  12111  tg2  12124  tgcl  12128  0nnei  12217  tgrest  12233  tgcn  12272  cnpnei  12283  cncnp2m  12295  lmtopcnp  12314  tx2cn  12334  txcn  12339  cnmpt21  12355  isxmet2d  12412  metrest  12570  metcnpi3  12581  tgioo  12610  fsumcncntop  12620  elcncf1di  12630  climcncf  12635  cncfco  12642  cnplimcim  12679  cnlimci  12685  bj-prexg  12911  peano5set  12940  bj-peano4  12955  bj-nn0suc  12964  bj-nn0sucALT  12978  bj-findis  12979  exmidsbthrlem  13019  trilpolemres  13037
  Copyright terms: Public domain W3C validator