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  389  sylan9r  390  imdistani  419  mpan10  443  anabsi5  513  anim12dan  532  pm3.43  534  con3and  563  imnan  623  jaoian  708  jaodan  709  impidc  754  pm2.5dc  762  con2bidc  768  pm5.18dc  776  dfandc  777  pm4.63dc  779  annimim  781  pm4.54dc  804  pm4.79dc  808  orcanai  836  annimdc  844  pm4.55dc  845  pm4.82  856  pm3.11dc  863  pm3.12dc  864  dn1dc  866  3jcad  1084  3expia  1105  3an1rs  1115  3imp1  1116  3imp2  1118  syl3anl2  1183  3jaoian  1199  3jaodan  1200  mp3anl1  1225  mp3anl2  1226  mp3anl3  1227  ecased  1238  xor3dc  1275  pm5.15dc  1277  xor2dc  1278  xornbidc  1279  xordc  1280  nbbndc  1282  biassdc  1283  bilukdc  1284  dfbi3dc  1285  pm5.24dc  1286  xordidc  1287  alanimi  1345  19.29  1508  equs4  1610  equsexd  1614  spimth  1620  equs5a  1672  ax11v2  1698  ax11b  1704  equs5or  1708  sb5rf  1729  equvin  1740  nfsb4t  1887  eu5  1944  mopick  1975  euexex  1982  2euswapdc  1988  exists2  1994  eqrdav  2036  dvelimdc  2194  nebidc  2279  pm13.18  2280  nelne1  2289  nelne2  2290  ralrimdvv  2397  r19.21bi  2401  r19.26  2435  ralbi  2439  rexbi  2440  r19.29  2444  vtoclgft  2598  rspcva  2648  rspc2va  2657  elabgt  2678  eqeu  2705  mob2  2715  mob  2717  euind  2722  reu6  2724  reuind  2738  sbctt  2818  rspsbca  2835  sbcnestgf  2891  rspcsbela  2899  ssel2  2934  sselda  2939  sstr  2947  nssne1  2995  nssne2  2996  reuss2  3211  reupick  3215  reupick2  3217  reximdva0m  3230  ssn0  3253  disjel  3268  ssdisj  3271  disjpss  3272  absneu  3433  preqr1g  3528  prel12  3533  dfiun2g  3680  nbrne1  3772  nbrne2  3773  mpteq12f  3828  triun  3858  csbexga  3876  iinexgm  3899  prexgOLD  3937  prexg  3938  copsex2t  3973  swopo  4034  poirr  4035  potr  4036  pofun  4040  issod  4047  ordelss  4082  trssord  4083  limelon  4102  trsuc  4125  eusvnfb  4152  rabxfrd  4167  regexmidlem1  4218  suc11g  4235  nnsuc  4281  brrelex12  4324  vtoclr  4331  optocl  4359  relop  4429  brcogw  4447  breldmg  4484  elreldm  4503  riinint  4536  issref  4650  xpidtr  4658  trin2  4659  cnveqb  4719  funopg  4877  funssres  4885  fununi  4910  funimass2  4920  imain  4924  fnun  4948  fco  4999  opelf  5005  f1oun  5089  fun11iun  5090  fv3  5140  ndmfvg  5147  fvelima  5168  fvopab3ig  5189  fvmptssdm  5198  fvmptf  5206  fvimacnv  5225  fmptco  5273  funfvima2  5334  funfvima3  5335  f1veqaeq  5351  f1ocnvfvrneq  5365  fliftfun  5379  isotr  5399  isoini  5400  isopolem  5404  isosolem  5406  moriotass  5439  acexmidlem2  5452  suppssfv  5650  suppssov1  5651  f1dmex  5685  releldm2  5753  f1o2ndf1  5791  poxp  5794  tposf2  5824  iunon  5840  smoel2  5859  tfrlem9  5876  tfrexlem  5889  tfri3  5894  sucinc2  5965  nnacom  6002  nnmcom  6007  nnsucsssuc  6010  nnaordi  6017  nnmordi  6025  nnaordex  6036  nnm00  6038  ectocld  6108  iinerm  6114  th3qlem2  6145  f1oen3g  6170  f1oeng  6173  en2d  6184  en3d  6185  dom2lem  6188  fundmen  6222  fundmeng  6223  unen  6229  xpdom2  6241  xpdom2g  6242  fopwdom  6246  ltmpig  6323  enq0sym  6414  addnq0mo  6429  mulnq0mo  6430  prarloclem3step  6478  prarloclem3  6479  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpdisj  6506  distrlem1prl  6556  distrlem1pru  6557  distrlem4prl  6558  distrlem4pru  6559  distrlem5prl  6560  distrlem5pru  6561  ltsopr  6568  ltaddpr  6569  addcanprleml  6586  addcanprlemu  6587  recexprlemm  6594  recexprlemlol  6596  recexprlemupu  6598  aptiprleml  6609  aptiprlemu  6610  addsrmo  6631  mulsrmo  6632  axprecex  6724  mulgt0  6850  ltne  6860  cnegexlem1  6943  cnegexlem2  6944  addgt0  7198  addgegt0  7199  addgtge0  7200  addge0  7201  recexre  7322  mulge0  7363  recexap  7376  prodgt02  7560  prodge02  7562  ltmul12a  7567  mulgt1  7570  nndivtr  7696  addltmul  7898  elnnnn0b  7962  elnnz  7991  zmulcl  8033  nn0n0n1ge2  8047  nn0lt2  8058  uzind2  8086  nn0ind-raph  8091  eluzp1m1  8232  uz3m2nn  8251  negm  8286  lbzbi  8287  qaddcl  8306  qmulcl  8308  qreccl  8311  xrltne  8459  xrre  8463  xrre2  8464  xrre3  8465  ge0gtmnf  8466  xltnegi  8478  iccsupr  8565  icoshft  8588  icoshftf1o  8589  fznlem  8635  fzen  8637  uzsubsubfz  8641  fzsuc2  8671  elfz1b  8682  elfz0ubfz0  8712  elfz0fzfz0  8713  fz0fzelfz0  8714  fz0fzdiffz0  8717  elfzmlbmOLD  8719  elfzmlbp  8720  difelfznle  8723  fzofzim  8774  eluzgtdifelfzo  8783  elfzodifsumelfzo  8787  elfzonlteqm1  8796  elfzom1p1elfzo  8800  ssfzo12bi  8811  frec2uzlt2d  8831  frecuzrdgfn  8839  m1expcl2  8891  expge1  8906  leexp2r  8922  expubnd  8925  zesq  8980  expnlbnd  8986  bj-prexg  9296  peano5set  9328  bj-peano4  9343  bj-nn0suc  9348  bj-nn0sucALT  9362  bj-findis  9363
  Copyright terms: Public domain W3C validator