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  560  anabsi5  581  anim12dan  604  pm3.43  606  con3dimp  640  annimim  693  imnan  697  jaoian  803  jaodan  805  stdcndc  853  impidc  866  pm2.5gdc  874  con2bidc  883  pm5.18dc  891  dfandc  892  pm4.63dc  894  pm4.54dc  910  pm4.79dc  911  orcanai  936  annimdc  946  pm4.55dc  947  orandc  948  pm4.82  959  pm3.11dc  966  pm3.12dc  967  dn1dc  969  3jcad  1205  3expia  1232  3an1rs  1246  3imp1  1247  3imp2  1249  syl3anl2  1323  3jaoian  1342  3jaodan  1343  mp3anl1  1368  mp3anl2  1369  mp3anl3  1370  ecased  1386  xor3dc  1432  pm5.15dc  1434  xor2dc  1435  xornbidc  1436  xordc  1437  nbbndc  1439  biassdc  1440  bilukdc  1441  dfbi3dc  1442  pm5.24dc  1443  xordidc  1444  alanimi  1508  19.29  1669  equs4  1773  equsexd  1778  spimth  1784  equs5a  1843  ax11v2  1869  ax11b  1875  equs5or  1879  sb5rf  1901  equvin  1912  nfsb4t  2068  eu5  2128  mopick  2159  euexex  2166  2euswapdc  2172  exists2  2178  eqrdav  2231  dvelimdc  2405  nebidc  2492  pm13.18  2493  nelne1  2502  nelne2  2503  rspa  2590  ralrimdvv  2626  r19.21bi  2630  r19.26  2669  ralbi  2675  rexbi  2676  r19.29  2680  vtoclgft  2864  rspcva  2918  rspc2va  2934  elabgt  2957  eqeu  2986  mob2  2996  mob  2998  euind  3003  reu6  3005  reuind  3021  sbctt  3108  rspsbca  3126  sbcnestgf  3189  rspcsbela  3197  ssel2  3232  sselda  3237  sstr  3245  nssne1  3295  nssne2  3296  reuss2  3500  reupick  3504  reupick2  3506  reximdva0m  3523  ssn0  3550  disjel  3562  ssdisj  3564  absneu  3762  preqr1g  3869  prel12  3874  dfiun2g  4022  nbrne1  4127  nbrne2  4128  mpteq12f  4189  triun  4220  csbexga  4237  prcssprc  4250  iinexgm  4265  prexg  4324  copsex2t  4360  swopo  4426  poirr  4427  potr  4428  pofun  4432  issod  4439  ordelss  4499  trssord  4500  limelon  4519  trsuc  4542  eusvnfb  4574  rabxfrd  4589  regexmidlem1  4654  nordeq  4665  suc11g  4678  nnsuc  4737  brrelex12  4787  vtoclr  4797  optocl  4825  relop  4904  brcogw  4923  breldmg  4961  elreldm  4982  riinint  5017  xpexcnvm  5116  issref  5144  xpidtr  5152  trin2  5153  cnveqb  5217  funopg  5385  funssres  5394  fununi  5423  funimass2  5433  imain  5437  fnun  5463  fco  5526  opelf  5534  f0rn0  5561  f1oun  5633  fun11iun  5634  fv3  5692  ndmfvg  5700  fvelima  5727  fvopab3ig  5750  fvmptssdm  5761  fvmptf  5769  fvimacnv  5792  fmptco  5842  fcof  5862  funfvima2  5918  funfvima3  5919  f1veqaeq  5941  f1ocnvfvrneq  5954  fliftfun  5968  isotr  5988  isoini  5990  isopolem  5994  isosolem  5996  moriotass  6033  acexmidlem2  6046  suppssov1  6262  f1dmex  6308  releldm2  6378  f1o2ndf1  6423  poxp  6427  fsuppeq  6446  suppssfvg  6462  tposf2  6498  iunon  6514  smoel2  6533  tfrlem9  6549  tfrexlem  6564  tfr1onlembxssdm  6573  tfr1onlemres  6579  tfrcllembxssdm  6586  tfrcllemres  6592  tfrcl  6594  tfri3  6597  frecabcl  6629  sucinc2  6678  nnacom  6716  nnmcom  6721  nnsucsssuc  6724  nnsucuniel  6727  nntri2or2  6730  nnaordi  6740  nnmordi  6748  nnaordex  6760  nnm00  6762  ectocld  6834  iinerm  6840  th3qlem2  6871  elpm2r  6899  mapsnd  6922  mapsncnv  6929  mptelixpg  6968  ixpsnf1o  6970  f1oen4g  6990  f1dom4g  6991  f1oen3g  6992  f1oeng  6995  en2d  7006  en3d  7007  dom2lem  7010  fundmen  7046  fundmeng  7047  unen  7057  modom  7060  rex2dom  7062  en2m  7065  xpdom2  7081  xpdom2g  7082  fopwdom  7088  nneneq  7110  phpm  7119  phpelm  7120  dif1enen  7136  fin0  7141  findcard  7144  diffifi  7150  ac6sfi  7154  onunsnss  7176  fiintim  7190  xpfi  7191  infidc  7200  fidcenum  7225  sbthlem1  7226  sbthlemi3  7228  sbthlemi10  7235  ffsuppbi  7252  elfir  7259  isotilem  7296  inflbti  7314  ordiso2  7325  eldju2ndl  7362  eldju2ndr  7363  updjudhf  7369  mkvprop  7448  carden2bex  7485  pm54.43  7486  exmidfodomrlemeldju  7501  exmidfodomrlemreseldju  7502  exmidfodomrlemim  7503  pw1m  7533  ltmpig  7650  enq0sym  7743  addnq0mo  7758  mulnq0mo  7759  prarloclem3step  7807  prarloclem3  7808  genpml  7828  genpmu  7829  genprndl  7832  genprndu  7833  genpdisj  7834  distrlem1prl  7893  distrlem1pru  7894  distrlem4prl  7895  distrlem4pru  7896  distrlem5prl  7897  distrlem5pru  7898  ltsopr  7907  ltaddpr  7908  addcanprleml  7925  addcanprlemu  7926  recexprlemm  7935  recexprlemlol  7937  recexprlemupu  7939  aptiprleml  7950  aptiprlemu  7951  caucvgprlemnkj  7977  caucvgprlemnbj  7978  addsrmo  8054  mulsrmo  8055  srpospr  8094  caucvgsr  8113  axprecex  8191  mpomulf  8260  mulgt0  8344  ltne  8354  cnegexlem1  8444  cnegexlem2  8445  negf1o  8651  addgt0  8718  addgegt0  8719  addgtge0  8720  addge0  8721  recexre  8848  mulge0  8889  recexap  8923  prodgt02  9123  prodge02  9125  ltmul12a  9130  mulgt1  9133  nndivtr  9275  addltmul  9471  elnnnn0b  9536  fcdmnn0supp  9544  fcdmnn0fsupp  9545  fcdmnn0suppg  9546  xnn0nnn0pnf  9572  elnnz  9583  zmulcl  9627  nn0n0n1ge2  9644  nn0lt2  9655  nn0le2is012  9656  uzind2  9686  nn0ind-raph  9691  eluzp1m1  9874  uz3m2nn  9901  supinfneg  9923  infsupneg  9924  infregelbex  9926  negm  9943  lbzbi  9944  qaddcl  9963  qmulcl  9965  qreccl  9970  elpq  9977  ledivge1le  10055  nn0ledivnn  10096  xrltne  10142  xrre  10149  xrre2  10150  xrre3  10151  ge0gtmnf  10152  xltnegi  10164  xnn0xadd0  10196  xnegdi  10197  xposdif  10211  xlesubadd  10212  iccsupr  10295  icoshft  10319  icoshftf1o  10320  fznlem  10371  fzen  10373  uzsubsubfz  10377  fzsuc2  10409  elfz1b  10420  elfz0ubfz0  10455  elfz0fzfz0  10456  fz0fzelfz0  10457  fz0fzdiffz0  10460  elfzmlbp  10462  difelfznle  10465  nn0p1elfzo  10517  fzofzim  10523  elincfzoext  10534  eluzgtdifelfzo  10538  elfzodifsumelfzo  10542  elfzonlteqm1  10551  elfzom1p1elfzo  10555  ssfzo12bi  10566  subfzo0  10584  zsupcllemex  10586  zssinfcl  10588  exbtwnzlemstep  10603  modqmuladdnn0  10726  modfzo0difsn  10753  addmodlteq  10756  frec2uzlt2d  10762  frecuzrdgtcl  10770  frecuzrdgfunlem  10777  seqf1og  10879  m1expcl2  10919  expge1  10934  leexp2r  10951  expubnd  10954  zesq  11016  expnlbnd  11022  nn0ltexp2  11067  nn0opthd  11080  faclbnd  11099  bcpasc  11124  hashprg  11168  seq3coll  11207  wrdnval  11248  wrdsymb0  11250  fstwrdne  11256  wrdred1hash  11261  swrdnd  11344  swrdwrdsymbg  11349  swrdsbslen  11351  swrdlsw  11354  swrdswrdlem  11389  swrdswrd  11390  pfxswrd  11391  cats1un  11406  wrd2ind  11408  swrdccatin1  11410  pfxccatin12lem4  11411  pfxccatin12lem2a  11412  pfxccatin12lem1  11413  swrdccatin2  11414  pfxccatin12lem2c  11415  pfxccatin12lem2  11416  pfxccatin12lem3  11417  pfxccatin12  11418  pfxccat3  11419  swrdccat  11420  pfxccat3a  11423  swrdccat3blem  11424  swrdccat3b  11425  swrdccatin2d  11429  reuccatpfxs1lem  11431  rexanuz  11666  rexuz3  11668  r19.29uz  11670  r19.2uz  11671  absnid  11751  leabs  11752  ltabs  11765  icodiamlt  11858  maxleast  11891  negfi  11906  climcn2  11987  climcau  12025  climcaucn  12029  sumdc  12036  fsum3cvg  12057  isumz  12068  fsumf1o  12069  fisumss  12071  isumss2  12072  fsumzcl2  12084  fsumsplit  12086  fsumsplitsnun  12098  sumsplitdc  12111  fsum2dlemstep  12113  telfsumo  12145  fsumparts  12149  fsumiun  12156  isumrpcl  12173  fproddccvg  12251  prod1dc  12265  prodssdc  12268  fprodssdc  12269  prodsnf  12271  fprodsplitdc  12275  fprod2dlemstep  12301  fprodmodd  12320  efexp  12361  efieq1re  12451  p1modz1  12473  dvds0lem  12480  dvds2ln  12503  dvdssub2  12514  dvdsadd2b  12519  dvdsabseq  12526  divconjdvds  12528  dvdsdivcl  12529  odd2np1  12552  oddge22np1  12560  opoe  12574  omoe  12575  opeo  12576  omeo  12577  m1expo  12579  nn0ehalf  12582  nn0o1gt2  12584  nno  12585  divalgb  12604  ndvdsadd  12610  bitsinv1lem  12640  gcd0id  12668  gcdneg  12671  gcdaddm  12673  bezoutlemstep  12686  dfgcd2  12703  gcddiv  12708  dvdsmulgcd  12714  bezoutr  12721  bezoutr1  12722  uzwodc  12726  nninfctlemfo  12729  algfx  12742  lcmgcdlem  12767  lcmgcdeq  12773  coprmdvds  12782  divgcdcoprmex  12792  cncongr1  12793  cncongr2  12794  isprm3  12808  dvdsnprmd  12815  prmgt1  12822  oddprmgt2  12824  isprm6  12837  cncongrprm  12847  phibndlem  12906  phimullem  12915  powm2modprm  12943  modprm0  12945  modprmn0modprm0  12947  prm23lt5  12954  pcneg  13016  pcprmpw2  13024  dvdsprmpweqnn  13027  dvdsprmpweqle  13028  pcaddlem  13030  fldivp1  13039  pcfac  13041  oddprmdvds  13045  prmunb  13053  ennnfone  13165  unct  13182  lidrididd  13584  gsummgmpropd  13596  sgrpass  13610  issgrpd  13614  issubmnd  13644  imasmnd2  13654  mnd1id  13658  insubm  13687  dfgrp2  13729  grpid  13741  grpasscan1  13765  dfgrp3mlem  13800  dfgrp3me  13802  imasgrp2  13816  mulgnn0gsum  13834  mulgnn0p1  13839  mulgaddcom  13852  mulginvcom  13853  mulgass  13865  mulgpropdg  13870  subginv  13887  issubg2m  13895  issubg4m  13899  grpissubg  13900  resgrpisgrp  13901  subgintm  13904  kerf1ghm  13980  cmncom  14008  imasabl  14042  rngdi  14073  rngdir  14074  rngpropd  14088  imasrng  14089  imasring  14197  nzrunit  14322  issubrng2  14344  subrngintm  14346  issubrg2  14375  subrgintm  14377  lmodfopnelem1  14459  lmodfopnelem2  14460  lmodfopne  14461  islssm  14492  islidlm  14614  rnglidlmcl  14615  dflidl2rng  14616  rnglidlmmgm  14631  rnglidlmsgrp  14632  rnglidlrng  14633  dvdsrzring  14738  znidom  14792  uniopn  14853  istopon  14865  fiinbas  14901  tg2  14912  tgcl  14916  0nnei  15005  tgrest  15021  tgcn  15060  cnpnei  15071  cncnp2m  15083  lmtopcnp  15102  tx2cn  15122  txcn  15127  cnmpt21  15143  isxmet2d  15200  metrest  15358  metcnpi3  15369  tgioo  15406  fsumcncntop  15419  elcncf1di  15431  climcncf  15436  cncfco  15443  suplociccreex  15476  cnplimcim  15519  cnlimci  15525  reeff1olem  15623  efltlemlt  15626  pellexlem1  15832  zabsle1  15859  lgslem3  15862  lgsmod  15886  lgsdir2lem5  15892  lgsdir2  15893  lgsne0  15898  lgsdirnn0  15907  gausslemma2dlem0f  15914  gausslemma2dlem1a  15918  gausslemma2dlem3  15923  2lgslem1c  15950  2lgslem3a1  15957  2lgslem3b1  15958  2lgslem3c1  15959  2lgslem3d1  15960  2lgslem3  15961  2lgsoddprmlem2  15966  uhgrm  16060  incistruhgr  16072  upgrfnen  16080  umgrfnen  16090  umgrnloop  16098  upgredgpr  16131  usgrausgrben  16154  usgredgop  16155  usgruspgrben  16168  usgrislfuspgrdom  16172  umgrvad2edg  16193  ushgredgedg  16208  ushgredgedgloop  16210  uhgr0v0e  16216  subgreldmiedg  16251  subupgr  16255  uhgrspansubgrlem  16258  vtxdg0v  16276  wlkpropg  16306  wlkvg  16310  wlkl1loop  16340  upgriswlkdc  16342  upgrwlkedg  16343  upgrwlkvtxedg  16346  uspgr2wlkeq  16347  wlkres  16361  trlf1  16370  clwwlk1loop  16381  clwwlkccatlem  16382  isclwwlknx  16398  clwwlkn1loopb  16402  clwwlkext2edg  16404  umgr2cwwk2dif  16406  clwwlknonex2lem2  16420  clwwlknonex2  16421  eupthseg  16434  eupth2lem3lem4fi  16455  bj-charfun  16564  bj-charfunr  16567  bj-charfunbi  16568  bj-prexg  16668  peano5set  16697  bj-peano4  16712  bj-nn0suc  16721  bj-nn0sucALT  16735  bj-findis  16736  exmidsbthrlem  16789  trilpolemres  16813  trirec0  16815  nconstwlpolem  16837  neapmkv  16840  gfsumval  16848