Theorem imp 124

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

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		imp.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	sylc 62	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  impcom  125  impd  254  imp31  256  imp32  257  expdimp  259  impancom  260  pm3.22  265  ancoms  268  adantr  276  impel  280  biimpa  296  biimpar  297  biimpac  298  biimparc  299  pm3.33  345  pm3.34  346  pm3.35  347  pm5.31  348  imp4b  350  imp41  353  imp42  354  imp43  355  imp44  356  imp45  357  imp5g  360  expr  375  impac  381  sylan9  409  sylan9r  410  imdistani  445  mpan10  474  adantl4r  517  adantl5r  525  adantl6r  526  a2and  558  anabsi5  579  anim12dan  602  pm3.43  604  con3dimp  638  annimim  690  imnan  694  jaoian  800  jaodan  802  stdcndc  850  impidc  863  pm2.5gdc  871  con2bidc  880  pm5.18dc  888  dfandc  889  pm4.63dc  891  pm4.54dc  907  pm4.79dc  908  orcanai  933  annimdc  943  pm4.55dc  944  orandc  945  pm4.82  956  pm3.11dc  963  pm3.12dc  964  dn1dc  966  3jcad  1202  3expia  1229  3an1rs  1243  3imp1  1244  3imp2  1246  syl3anl2  1320  3jaoian  1339  3jaodan  1340  mp3anl1  1365  mp3anl2  1366  mp3anl3  1367  ecased  1383  xor3dc  1429  pm5.15dc  1431  xor2dc  1432  xornbidc  1433  xordc  1434  nbbndc  1436  biassdc  1437  bilukdc  1438  dfbi3dc  1439  pm5.24dc  1440  xordidc  1441  alanimi  1505  19.29  1666  equs4  1771  equsexd  1775  spimth  1781  equs5a  1840  ax11v2  1866  ax11b  1872  equs5or  1876  sb5rf  1898  equvin  1909  nfsb4t  2065  eu5  2125  mopick  2156  euexex  2163  2euswapdc  2169  exists2  2175  eqrdav  2228  dvelimdc  2393  nebidc  2480  pm13.18  2481  nelne1  2490  nelne2  2491  rspa  2578  ralrimdvv  2614  r19.21bi  2618  r19.26  2657  ralbi  2663  rexbi  2664  r19.29  2668  vtoclgft  2851  rspcva  2905  rspc2va  2921  elabgt  2944  eqeu  2973  mob2  2983  mob  2985  euind  2990  reu6  2992  reuind  3008  sbctt  3095  rspsbca  3113  sbcnestgf  3176  rspcsbela  3184  ssel2  3219  sselda  3224  sstr  3232  nssne1  3282  nssne2  3283  reuss2  3484  reupick  3488  reupick2  3490  reximdva0m  3507  ssn0  3534  disjel  3546  ssdisj  3548  absneu  3738  preqr1g  3844  prel12  3849  dfiun2g  3997  nbrne1  4102  nbrne2  4103  mpteq12f  4164  triun  4195  csbexga  4212  iinexgm  4238  prexg  4295  copsex2t  4331  swopo  4397  poirr  4398  potr  4399  pofun  4403  issod  4410  ordelss  4470  trssord  4471  limelon  4490  trsuc  4513  eusvnfb  4545  rabxfrd  4560  regexmidlem1  4625  nordeq  4636  suc11g  4649  nnsuc  4708  brrelex12  4757  vtoclr  4767  optocl  4795  relop  4872  brcogw  4891  breldmg  4929  elreldm  4950  riinint  4985  issref  5111  xpidtr  5119  trin2  5120  cnveqb  5184  funopg  5352  funssres  5360  fununi  5389  funimass2  5399  imain  5403  fnun  5429  fco  5491  opelf  5498  f0rn0  5522  f1oun  5594  fun11iun  5595  fv3  5652  ndmfvg  5660  fvelima  5687  fvopab3ig  5710  fvmptssdm  5721  fvmptf  5729  fvimacnv  5752  fmptco  5803  fcof  5822  funfvima2  5876  funfvima3  5877  f1veqaeq  5899  f1ocnvfvrneq  5912  fliftfun  5926  isotr  5946  isoini  5948  isopolem  5952  isosolem  5954  moriotass  5991  acexmidlem2  6004  suppssfv  6220  suppssov1  6221  f1dmex  6267  releldm2  6337  f1o2ndf1  6380  poxp  6384  tposf2  6420  iunon  6436  smoel2  6455  tfrlem9  6471  tfrexlem  6486  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfrcllembxssdm  6508  tfrcllemres  6514  tfrcl  6516  tfri3  6519  frecabcl  6551  sucinc2  6600  nnacom  6638  nnmcom  6643  nnsucsssuc  6646  nnsucuniel  6649  nntri2or2  6652  nnaordi  6662  nnmordi  6670  nnaordex  6682  nnm00  6684  ectocld  6756  iinerm  6762  th3qlem2  6793  elpm2r  6821  mapsncnv  6850  mptelixpg  6889  ixpsnf1o  6891  f1oen4g  6911  f1dom4g  6912  f1oen3g  6913  f1oeng  6916  en2d  6927  en3d  6928  dom2lem  6931  fundmen  6967  fundmeng  6968  unen  6977  rex2dom  6979  en2m  6982  xpdom2  6998  xpdom2g  6999  fopwdom  7005  nneneq  7026  phpm  7035  phpelm  7036  dif1enen  7050  fin0  7055  findcard  7058  diffifi  7064  ac6sfi  7068  onunsnss  7087  fiintim  7101  xpfi  7102  infidc  7109  fidcenum  7131  sbthlem1  7132  sbthlemi3  7134  sbthlemi10  7141  elfir  7148  isotilem  7181  inflbti  7199  ordiso2  7210  eldju2ndl  7247  eldju2ndr  7248  updjudhf  7254  mkvprop  7333  carden2bex  7370  pm54.43  7371  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  exmidfodomrlemim  7387  pw1m  7417  ltmpig  7534  enq0sym  7627  addnq0mo  7642  mulnq0mo  7643  prarloclem3step  7691  prarloclem3  7692  genpml  7712  genpmu  7713  genprndl  7716  genprndu  7717  genpdisj  7718  distrlem1prl  7777  distrlem1pru  7778  distrlem4prl  7779  distrlem4pru  7780  distrlem5prl  7781  distrlem5pru  7782  ltsopr  7791  ltaddpr  7792  addcanprleml  7809  addcanprlemu  7810  recexprlemm  7819  recexprlemlol  7821  recexprlemupu  7823  aptiprleml  7834  aptiprlemu  7835  caucvgprlemnkj  7861  caucvgprlemnbj  7862  addsrmo  7938  mulsrmo  7939  srpospr  7978  caucvgsr  7997  axprecex  8075  mpomulf  8144  mulgt0  8229  ltne  8239  cnegexlem1  8329  cnegexlem2  8330  negf1o  8536  addgt0  8603  addgegt0  8604  addgtge0  8605  addge0  8606  recexre  8733  mulge0  8774  recexap  8808  prodgt02  9008  prodge02  9010  ltmul12a  9015  mulgt1  9018  nndivtr  9160  addltmul  9356  elnnnn0b  9421  xnn0nnn0pnf  9453  elnnz  9464  zmulcl  9508  nn0n0n1ge2  9525  nn0lt2  9536  nn0le2is012  9537  uzind2  9567  nn0ind-raph  9572  eluzp1m1  9754  uz3m2nn  9776  supinfneg  9798  infsupneg  9799  infregelbex  9801  negm  9818  lbzbi  9819  qaddcl  9838  qmulcl  9840  qreccl  9845  elpq  9852  ledivge1le  9930  nn0ledivnn  9971  xrltne  10017  xrre  10024  xrre2  10025  xrre3  10026  ge0gtmnf  10027  xltnegi  10039  xnn0xadd0  10071  xnegdi  10072  xposdif  10086  xlesubadd  10087  iccsupr  10170  icoshft  10194  icoshftf1o  10195  fznlem  10245  fzen  10247  uzsubsubfz  10251  fzsuc2  10283  elfz1b  10294  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  fz0fzdiffz0  10334  elfzmlbp  10336  difelfznle  10339  fzofzim  10396  elincfzoext  10407  eluzgtdifelfzo  10411  elfzodifsumelfzo  10415  elfzonlteqm1  10424  elfzom1p1elfzo  10428  ssfzo12bi  10439  subfzo0  10456  zsupcllemex  10458  zssinfcl  10460  exbtwnzlemstep  10475  modqmuladdnn0  10598  modfzo0difsn  10625  addmodlteq  10628  frec2uzlt2d  10634  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  seqf1og  10751  m1expcl2  10791  expge1  10806  leexp2r  10823  expubnd  10826  zesq  10888  expnlbnd  10894  nn0ltexp2  10939  nn0opthd  10952  faclbnd  10971  bcpasc  10996  hashprg  11038  seq3coll  11072  wrdnval  11110  wrdsymb0  11112  fstwrdne  11118  wrdred1hash  11123  swrdnd  11199  swrdwrdsymbg  11204  swrdsbslen  11206  swrdlsw  11209  swrdswrdlem  11244  swrdswrd  11245  pfxswrd  11246  cats1un  11261  wrd2ind  11263  swrdccatin1  11265  pfxccatin12lem4  11266  pfxccatin12lem2a  11267  pfxccatin12lem1  11268  swrdccatin2  11269  pfxccatin12lem2c  11270  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccatin12  11273  pfxccat3  11274  swrdccat  11275  pfxccat3a  11278  swrdccat3blem  11279  swrdccat3b  11280  swrdccatin2d  11284  reuccatpfxs1lem  11286  rexanuz  11507  rexuz3  11509  r19.29uz  11511  r19.2uz  11512  absnid  11592  leabs  11593  ltabs  11606  icodiamlt  11699  maxleast  11732  negfi  11747  climcn2  11828  climcau  11866  climcaucn  11870  sumdc  11877  fsum3cvg  11897  isumz  11908  fsumf1o  11909  fisumss  11911  isumss2  11912  fsumzcl2  11924  fsumsplit  11926  fsumsplitsnun  11938  sumsplitdc  11951  fsum2dlemstep  11953  telfsumo  11985  fsumparts  11989  fsumiun  11996  isumrpcl  12013  fproddccvg  12091  prod1dc  12105  prodssdc  12108  fprodssdc  12109  prodsnf  12111  fprodsplitdc  12115  fprod2dlemstep  12141  fprodmodd  12160  efexp  12201  efieq1re  12291  p1modz1  12313  dvds0lem  12320  dvds2ln  12343  dvdssub2  12354  dvdsadd2b  12359  dvdsabseq  12366  divconjdvds  12368  dvdsdivcl  12369  odd2np1  12392  oddge22np1  12400  opoe  12414  omoe  12415  opeo  12416  omeo  12417  m1expo  12419  nn0ehalf  12422  nn0o1gt2  12424  nno  12425  divalgb  12444  ndvdsadd  12450  bitsinv1lem  12480  gcd0id  12508  gcdneg  12511  gcdaddm  12513  bezoutlemstep  12526  dfgcd2  12543  gcddiv  12548  dvdsmulgcd  12554  bezoutr  12561  bezoutr1  12562  uzwodc  12566  nninfctlemfo  12569  algfx  12582  lcmgcdlem  12607  lcmgcdeq  12613  coprmdvds  12622  divgcdcoprmex  12632  cncongr1  12633  cncongr2  12634  isprm3  12648  dvdsnprmd  12655  prmgt1  12662  oddprmgt2  12664  isprm6  12677  cncongrprm  12687  phibndlem  12746  phimullem  12755  powm2modprm  12783  modprm0  12785  modprmn0modprm0  12787  prm23lt5  12794  pcneg  12856  pcprmpw2  12864  dvdsprmpweqnn  12867  dvdsprmpweqle  12868  pcaddlem  12870  fldivp1  12879  pcfac  12881  oddprmdvds  12885  prmunb  12893  ennnfone  13004  unct  13021  lidrididd  13423  gsummgmpropd  13435  sgrpass  13449  issgrpd  13453  issubmnd  13483  imasmnd2  13493  mnd1id  13497  insubm  13526  dfgrp2  13568  grpid  13580  grpasscan1  13604  dfgrp3mlem  13639  dfgrp3me  13641  imasgrp2  13655  mulgnn0gsum  13673  mulgnn0p1  13678  mulgaddcom  13691  mulginvcom  13692  mulgass  13704  mulgpropdg  13709  subginv  13726  issubg2m  13734  issubg4m  13738  grpissubg  13739  resgrpisgrp  13740  subgintm  13743  kerf1ghm  13819  cmncom  13847  imasabl  13881  rngdi  13911  rngdir  13912  rngpropd  13926  imasrng  13927  imasring  14035  nzrunit  14160  issubrng2  14182  subrngintm  14184  issubrg2  14213  subrgintm  14215  lmodfopnelem1  14296  lmodfopnelem2  14297  lmodfopne  14298  islssm  14329  islidlm  14451  rnglidlmcl  14452  dflidl2rng  14453  rnglidlmmgm  14468  rnglidlmsgrp  14469  rnglidlrng  14470  dvdsrzring  14575  znidom  14629  uniopn  14683  istopon  14695  fiinbas  14731  tg2  14742  tgcl  14746  0nnei  14835  tgrest  14851  tgcn  14890  cnpnei  14901  cncnp2m  14913  lmtopcnp  14932  tx2cn  14952  txcn  14957  cnmpt21  14973  isxmet2d  15030  metrest  15188  metcnpi3  15199  tgioo  15236  fsumcncntop  15249  elcncf1di  15261  climcncf  15266  cncfco  15273  suplociccreex  15306  cnplimcim  15349  cnlimci  15355  reeff1olem  15453  efltlemlt  15456  zabsle1  15686  lgslem3  15689  lgsmod  15713  lgsdir2lem5  15719  lgsdir2  15720  lgsne0  15725  lgsdirnn0  15734  gausslemma2dlem0f  15741  gausslemma2dlem1a  15745  gausslemma2dlem3  15750  2lgslem1c  15777  2lgslem3a1  15784  2lgslem3b1  15785  2lgslem3c1  15786  2lgslem3d1  15787  2lgslem3  15788  2lgsoddprmlem2  15793  uhgrm  15886  incistruhgr  15898  upgrfnen  15906  umgrfnen  15916  umgrnloop  15924  upgredgpr  15955  usgrausgrben  15978  usgredgop  15979  usgruspgrben  15992  usgrislfuspgrdom  15996  umgrvad2edg  16017  ushgredgedg  16032  ushgredgedgloop  16034  wlkpropg  16045  wlkvg  16049  wlkl1loop  16079  upgriswlkdc  16081  upgrwlkedg  16082  upgrwlkvtxedg  16085  uspgr2wlkeq  16086  wlkres  16098  trlf1  16106  bj-charfun  16194  bj-charfunr  16197  bj-charfunbi  16198  bj-prexg  16298  peano5set  16327  bj-peano4  16342  bj-nn0suc  16351  bj-nn0sucALT  16365  bj-findis  16366  exmidsbthrlem  16420  trilpolemres  16440  trirec0  16442  nconstwlpolem  16463  neapmkv  16466