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

Theorem imp 122
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 107 . 2 ((𝜑𝜓) → 𝜑)
2 simpr 108 . 2 ((𝜑𝜓) → 𝜓)
3 imp.1 . 2 (𝜑 → (𝜓𝜒))
41, 2, 3sylc 61 1 ((𝜑𝜓) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem is referenced by:  impcom  123  impd  251  imp31  252  imp32  253  expdimp  255  impancom  256  pm3.22  261  ancoms  264  adantr  270  impel  274  biimpa  290  biimpar  291  biimpac  292  biimparc  293  pm3.33  337  pm3.34  338  pm3.35  339  pm5.31  340  imp4b  342  imp41  345  imp42  346  imp43  347  imp44  348  imp45  349  imp5g  352  expr  367  impac  373  sylan9  401  sylan9r  402  imdistani  434  mpan10  458  anabsi5  544  anim12dan  565  pm3.43  567  con3dimp  597  imnan  657  jaoian  742  jaodan  744  impidc  789  pm2.5dc  797  con2bidc  803  pm5.18dc  811  dfandc  812  pm4.63dc  814  annimim  816  pm4.54dc  839  pm4.79dc  843  orcanai  871  annimdc  879  pm4.55dc  880  orandc  881  pm4.82  892  pm3.11dc  899  pm3.12dc  900  dn1dc  902  3jcad  1120  3expia  1141  3an1rs  1151  3imp1  1152  3imp2  1154  syl3anl2  1219  3jaoian  1237  3jaodan  1238  mp3anl1  1263  mp3anl2  1264  mp3anl3  1265  ecased  1281  xor3dc  1319  pm5.15dc  1321  xor2dc  1322  xornbidc  1323  xordc  1324  nbbndc  1326  biassdc  1327  bilukdc  1328  dfbi3dc  1329  pm5.24dc  1330  xordidc  1331  alanimi  1389  19.29  1552  equs4  1654  equsexd  1658  spimth  1664  equs5a  1716  ax11v2  1742  ax11b  1748  equs5or  1752  sb5rf  1774  equvin  1785  nfsb4t  1932  eu5  1989  mopick  2020  euexex  2027  2euswapdc  2033  exists2  2039  eqrdav  2081  dvelimdc  2239  nebidc  2326  pm13.18  2327  nelne1  2336  nelne2  2337  ralrimdvv  2446  r19.21bi  2450  r19.26  2486  ralbi  2490  rexbi  2491  r19.29  2495  vtoclgft  2650  rspcva  2700  rspc2va  2715  elabgt  2736  eqeu  2763  mob2  2773  mob  2775  euind  2780  reu6  2782  reuind  2796  sbctt  2881  rspsbca  2898  sbcnestgf  2954  rspcsbela  2962  ssel2  2995  sselda  3000  sstr  3008  nssne1  3056  nssne2  3057  reuss2  3251  reupick  3255  reupick2  3257  reximdva0m  3270  ssn0  3293  disjel  3305  ssdisj  3307  absneu  3472  preqr1g  3566  prel12  3571  dfiun2g  3718  nbrne1  3810  nbrne2  3811  mpteq12f  3866  triun  3896  csbexga  3914  iinexgm  3937  prexg  3974  copsex2t  4008  swopo  4069  poirr  4070  potr  4071  pofun  4075  issod  4082  ordelss  4142  trssord  4143  limelon  4162  trsuc  4185  eusvnfb  4212  rabxfrd  4227  regexmidlem1  4284  nordeq  4295  suc11g  4308  nnsuc  4364  brrelex12  4407  vtoclr  4414  optocl  4442  relop  4514  brcogw  4532  breldmg  4569  elreldm  4588  riinint  4621  issref  4737  xpidtr  4745  trin2  4746  cnveqb  4806  funopg  4964  funssres  4972  fununi  4998  funimass2  5008  imain  5012  fnun  5036  fco  5087  opelf  5093  f1oun  5177  fun11iun  5178  fv3  5229  ndmfvg  5236  fvelima  5257  fvopab3ig  5278  fvmptssdm  5287  fvmptf  5295  fvimacnv  5314  fmptco  5362  funfvima2  5423  funfvima3  5424  f1veqaeq  5440  f1ocnvfvrneq  5453  fliftfun  5467  isotr  5487  isoini  5488  isopolem  5492  isosolem  5494  moriotass  5527  acexmidlem2  5540  suppssfv  5739  suppssov1  5740  f1dmex  5774  releldm2  5842  f1o2ndf1  5880  poxp  5884  tposf2  5917  iunon  5933  smoel2  5952  tfrlem9  5968  tfrexlem  5983  tfr1onlembxssdm  5992  tfr1onlemres  5998  tfrcllembxssdm  6005  tfrcllemres  6011  tfrcl  6013  tfri3  6016  frecabcl  6048  sucinc2  6090  nnacom  6128  nnmcom  6133  nnsucsssuc  6136  nnsucuniel  6139  nntri2or2  6142  nnaordi  6147  nnmordi  6155  nnaordex  6166  nnm00  6168  ectocld  6238  iinerm  6244  th3qlem2  6275  f1oen3g  6301  f1oeng  6304  en2d  6315  en3d  6316  dom2lem  6319  fundmen  6353  fundmeng  6354  unen  6361  xpdom2  6375  xpdom2g  6376  fopwdom  6380  nneneq  6392  phpm  6400  phpelm  6401  fin0  6419  findcard  6422  diffifi  6428  ac6sfi  6431  onunsnss  6437  isotilem  6478  inflbti  6496  ordiso2  6505  carden2bex  6517  pm54.43  6518  ltmpig  6591  enq0sym  6684  addnq0mo  6699  mulnq0mo  6700  prarloclem3step  6748  prarloclem3  6749  genpml  6769  genpmu  6770  genprndl  6773  genprndu  6774  genpdisj  6775  distrlem1prl  6834  distrlem1pru  6835  distrlem4prl  6836  distrlem4pru  6837  distrlem5prl  6838  distrlem5pru  6839  ltsopr  6848  ltaddpr  6849  addcanprleml  6866  addcanprlemu  6867  recexprlemm  6876  recexprlemlol  6878  recexprlemupu  6880  aptiprleml  6891  aptiprlemu  6892  caucvgprlemnkj  6918  caucvgprlemnbj  6919  addsrmo  6982  mulsrmo  6983  srpospr  7021  caucvgsr  7040  axprecex  7108  mulgt0  7253  ltne  7263  cnegexlem1  7350  cnegexlem2  7351  negf1o  7553  addgt0  7619  addgegt0  7620  addgtge0  7621  addge0  7622  recexre  7745  mulge0  7786  recexap  7810  prodgt02  7998  prodge02  8000  ltmul12a  8005  mulgt1  8008  nndivtr  8147  addltmul  8334  elnnnn0b  8399  xnn0nnn0pnf  8431  elnnz  8442  zmulcl  8485  nn0n0n1ge2  8499  nn0lt2  8510  uzind2  8540  nn0ind-raph  8545  eluzp1m1  8723  uz3m2nn  8742  supinfneg  8764  infsupneg  8765  negm  8781  lbzbi  8782  qaddcl  8801  qmulcl  8803  qreccl  8808  ledivge1le  8884  nn0ledivnn  8919  xrltne  8959  xrre  8963  xrre2  8964  xrre3  8965  ge0gtmnf  8966  xltnegi  8978  iccsupr  9065  icoshft  9088  icoshftf1o  9089  fznlem  9136  fzen  9138  uzsubsubfz  9142  fzsuc2  9172  elfz1b  9183  elfz0ubfz0  9213  elfz0fzfz0  9214  fz0fzelfz0  9215  fz0fzdiffz0  9218  elfzmlbp  9220  difelfznle  9223  fzofzim  9274  eluzgtdifelfzo  9283  elfzodifsumelfzo  9287  elfzonlteqm1  9296  elfzom1p1elfzo  9300  ssfzo12bi  9311  subfzo0  9328  exbtwnzlemstep  9334  modqmuladdnn0  9450  modfzo0difsn  9477  addmodlteq  9480  frec2uzlt2d  9486  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  iseqid3  9561  m1expcl2  9595  expge1  9610  leexp2r  9627  expubnd  9630  zesq  9688  expnlbnd  9694  nn0opthd  9746  faclbnd  9765  bcpasc  9790  sizeprg  9832  rexanuz  10012  rexuz3  10014  r19.29uz  10016  r19.2uz  10017  absnid  10097  leabs  10098  ltabs  10111  icodiamlt  10204  maxleast  10237  negfi  10248  climcn2  10286  climcau  10322  climcaucn  10326  sumdc  10333  fisumcvg  10338  dvds0lem  10350  dvds2ln  10373  dvdssub2  10382  dvdsadd2b  10387  dvdsabseq  10392  divconjdvds  10394  dvdsdivcl  10395  odd2np1  10417  oddge22np1  10425  opoe  10439  omoe  10440  opeo  10441  omeo  10442  m1expo  10444  nn0ehalf  10447  nn0o1gt2  10449  nno  10450  divalgb  10469  ndvdsadd  10475  zsupcllemex  10486  zssinfcl  10488  gcd0id  10514  gcdneg  10517  gcdaddm  10519  bezoutlemstep  10530  dfgcd2  10547  gcddiv  10552  dvdsmulgcd  10558  bezoutr  10565  bezoutr1  10566  ialgfx  10578  lcmgcdlem  10603  lcmgcdeq  10609  coprmdvds  10618  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  isprm3  10644  dvdsnprmd  10651  prmgt1  10657  oddprmgt2  10659  isprm6  10670  cncongrprm  10680  bj-prexg  10887  peano5set  10920  bj-peano4  10935  bj-nn0suc  10944  bj-nn0sucALT  10958  bj-findis  10959
  Copyright terms: Public domain W3C validator