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

Theorem imp 115
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 102 . 2 ((φ ψ) → φ)
2 simpr 103 . 2 ((φ ψ) → ψ)
3 imp.1 . 2 (φ → (ψχ))
41, 2, 3sylc 56 1 ((φ ψ) → χ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem is referenced by:  impcom  116  impd  242  imp31  243  imp32  244  expdimp  246  impancom  247  pm3.22  252  ancoms  255  adantr  261  biimpa  280  biimpar  281  biimpac  282  biimparc  283  pm3.33  327  pm3.34  328  pm3.35  329  pm5.31  330  imp4b  332  imp41  335  imp42  336  imp43  337  imp44  338  imp45  339  imp5g  342  expr  357  impac  363  sylan9  391  sylan9r  392  imdistani  422  mpan10  446  anabsi5  500  anim12dan  519  pm3.43  521  con3and  551  imnan  611  jaoian  696  jaodan  697  impidc  743  pm2.5dc  751  con2bidc  757  pm5.18dc  765  dfandc  766  pm4.63dc  768  annimim  770  pm4.54dc  793  pm4.79dc  797  orcanai  823  annimdc  831  pm4.55dc  832  pm4.82  843  pm3.11dc  850  pm3.12dc  851  dn1dc  853  3jcad  1068  3expia  1090  3an1rs  1100  3imp1  1101  3imp2  1103  syl3anl2  1168  3jaoian  1184  3jaodan  1185  mp3anl1  1209  mp3anl2  1210  mp3anl3  1211  ecased  1222  xor3dc  1259  pm5.15dc  1261  xor2dc  1262  xornbidc  1263  xordc  1264  nbbndc  1266  biassdc  1267  bilukdc  1268  dfbi3dc  1269  pm5.24dc  1270  xordidc  1271  alanimi  1324  19.29  1489  equs4  1591  equsexd  1595  spimth  1601  equs5a  1653  ax11v2  1679  ax11b  1685  equs5or  1689  sb5rf  1710  equvin  1721  nfsb4t  1868  eu5  1925  mopick  1956  euexex  1963  2euswapdc  1969  exists2  1975  eqrdav  2017  dvelimdc  2175  nebidc  2259  pm13.18  2260  nelne1  2269  nelne2  2270  ralrimdvv  2377  r19.21bi  2381  r19.26  2415  ralbi  2419  rexbi  2420  r19.29  2424  vtoclgft  2577  rspcva  2627  rspc2va  2636  elabgt  2657  eqeu  2684  mob2  2694  mob  2696  euind  2701  reu6  2703  reuind  2717  sbctt  2797  rspsbca  2814  sbcnestgf  2870  rspcsbela  2878  ssel2  2913  sselda  2918  sstr  2926  nssne1  2974  nssne2  2975  reuss2  3190  reupick  3194  reupick2  3196  reximdva0m  3209  ssn0  3232  disjel  3247  ssdisj  3250  disjpss  3251  absneu  3412  preqr1g  3507  prel12  3512  dfiun2g  3659  nbrne1  3751  nbrne2  3752  mpteq12f  3807  triun  3837  csbexgOLD  3855  iinexgm  3878  prexgOLD  3916  prexg  3917  copsex2t  3952  swopo  4013  poirr  4014  potr  4015  pofun  4019  issod  4026  ordelss  4061  trssord  4062  limelon  4081  trsuc  4105  eusvnfb  4132  rabxfrd  4147  regexmidlem1  4198  suc11g  4215  nnsuc  4261  brrelex12  4304  vtoclr  4311  optocl  4339  relop  4409  brcogw  4427  breldmg  4464  elreldm  4483  riinint  4516  issref  4630  xpidtr  4638  trin2  4639  cnveqb  4699  funopg  4856  funssres  4864  fununi  4889  funimass2  4899  imain  4903  fnun  4927  fco  4977  opelf  4983  f1oun  5067  fun11iun  5068  fv3  5118  ndmfvg  5125  fvelima  5146  fvopab3ig  5167  fvmptssdm  5176  fvmptf  5184  fvimacnv  5203  fmptco  5251  funfvima2  5312  funfvima3  5313  f1veqaeq  5329  f1ocnvfvrneq  5343  fliftfun  5357  isotr  5377  isoini  5378  isopolem  5382  isosolem  5384  moriotass  5416  acexmidlem2  5429  suppssfv  5627  suppssov1  5628  f1dmex  5662  releldm2  5730  f1o2ndf1  5768  poxp  5771  tposf2  5801  iunon  5817  smoel2  5836  tfrlem9  5853  tfrexlem  5866  tfri3  5871  sucinc2  5937  nnacom  5974  nnmcom  5979  nnsucsssuc  5982  nnaordi  5988  nnmordi  5996  nnaordex  6007  nnm00  6009  ectocld  6079  iinerm  6085  th3qlem2  6116  ltmpig  6193  enq0sym  6281  addnq0mo  6296  mulnq0mo  6297  prarloclem3step  6344  prarloclem3  6345  genpml  6366  genpmu  6367  genprndl  6370  genprndu  6371  genpdisj  6372  distrlem1prl  6415  distrlem1pru  6416  distrlem4prl  6417  distrlem4pru  6418  distrlem5prl  6419  distrlem5pru  6420  ltsopr  6427  ltaddpr  6428  addcanprleml  6445  addcanprlemu  6446  recexprlemm  6452  recexprlemlol  6454  recexprlemupu  6456  addsrmo  6484  mulsrmo  6485  axprecex  6568  mulgt0  6687  ltne  6695  cnegexlem1  6773  cnegexlem2  6774  addgt0  7028  addgegt0  7029  addgtge0  7030  addge0  7031  bj-prexg  7273  peano5set  7301  bj-peano4  7316  bj-nn0suc  7321  bj-nn0sucALT  7335  bj-findis  7336
  Copyright terms: Public domain W3C validator