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  6415  addnq0mo  6430  mulnq0mo  6431  prarloclem3step  6479  prarloclem3  6480  genpml  6500  genpmu  6501  genprndl  6504  genprndu  6505  genpdisj  6506  distrlem1prl  6558  distrlem1pru  6559  distrlem4prl  6560  distrlem4pru  6561  distrlem5prl  6562  distrlem5pru  6563  ltsopr  6570  ltaddpr  6571  addcanprleml  6588  addcanprlemu  6589  recexprlemm  6596  recexprlemlol  6598  recexprlemupu  6600  aptiprleml  6611  aptiprlemu  6612  caucvgprlemnkj  6637  caucvgprlemnbj  6638  addsrmo  6671  mulsrmo  6672  axprecex  6764  mulgt0  6890  ltne  6900  cnegexlem1  6983  cnegexlem2  6984  addgt0  7238  addgegt0  7239  addgtge0  7240  addge0  7241  recexre  7362  mulge0  7403  recexap  7416  prodgt02  7600  prodge02  7602  ltmul12a  7607  mulgt1  7610  nndivtr  7736  addltmul  7938  elnnnn0b  8002  elnnz  8031  zmulcl  8073  nn0n0n1ge2  8087  nn0lt2  8098  uzind2  8126  nn0ind-raph  8131  eluzp1m1  8272  uz3m2nn  8291  negm  8326  lbzbi  8327  qaddcl  8346  qmulcl  8348  qreccl  8351  xrltne  8499  xrre  8503  xrre2  8504  xrre3  8505  ge0gtmnf  8506  xltnegi  8518  iccsupr  8605  icoshft  8628  icoshftf1o  8629  fznlem  8675  fzen  8677  uzsubsubfz  8681  fzsuc2  8711  elfz1b  8722  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  difelfznle  8763  fzofzim  8814  eluzgtdifelfzo  8823  elfzodifsumelfzo  8827  elfzonlteqm1  8836  elfzom1p1elfzo  8840  ssfzo12bi  8851  frec2uzlt2d  8871  frecuzrdgfn  8879  m1expcl2  8931  expge1  8946  leexp2r  8962  expubnd  8965  zesq  9020  expnlbnd  9026  absnid  9227  bj-prexg  9366  peano5set  9399  peano5setOLD  9400  bj-peano4  9415  bj-nn0suc  9424  bj-nn0sucALT  9438  bj-findis  9439
  Copyright terms: Public domain W3C validator