ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imp Structured version   Unicode 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  6499  genpmu  6500  genprndl  6503  genprndu  6504  genpdisj  6505  distrlem1prl  6557  distrlem1pru  6558  distrlem4prl  6559  distrlem4pru  6560  distrlem5prl  6561  distrlem5pru  6562  ltsopr  6569  ltaddpr  6570  addcanprleml  6587  addcanprlemu  6588  recexprlemm  6595  recexprlemlol  6597  recexprlemupu  6599  aptiprleml  6610  aptiprlemu  6611  addsrmo  6651  mulsrmo  6652  axprecex  6744  mulgt0  6870  ltne  6880  cnegexlem1  6963  cnegexlem2  6964  addgt0  7218  addgegt0  7219  addgtge0  7220  addge0  7221  recexre  7342  mulge0  7383  recexap  7396  prodgt02  7580  prodge02  7582  ltmul12a  7587  mulgt1  7590  nndivtr  7716  addltmul  7918  elnnnn0b  7982  elnnz  8011  zmulcl  8053  nn0n0n1ge2  8067  nn0lt2  8078  uzind2  8106  nn0ind-raph  8111  eluzp1m1  8252  uz3m2nn  8271  negm  8306  lbzbi  8307  qaddcl  8326  qmulcl  8328  qreccl  8331  xrltne  8479  xrre  8483  xrre2  8484  xrre3  8485  ge0gtmnf  8486  xltnegi  8498  iccsupr  8585  icoshft  8608  icoshftf1o  8609  fznlem  8655  fzen  8657  uzsubsubfz  8661  fzsuc2  8691  elfz1b  8702  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  difelfznle  8743  fzofzim  8794  eluzgtdifelfzo  8803  elfzodifsumelfzo  8807  elfzonlteqm1  8816  elfzom1p1elfzo  8820  ssfzo12bi  8831  frec2uzlt2d  8851  frecuzrdgfn  8859  m1expcl2  8911  expge1  8926  leexp2r  8942  expubnd  8945  zesq  9000  expnlbnd  9006  absnid  9207  bj-prexg  9342  peano5set  9374  bj-peano4  9389  bj-nn0suc  9394  bj-nn0sucALT  9408  bj-findis  9409
  Copyright terms: Public domain W3C validator