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  600  pm3.43  602  con3dimp  635  annimim  686  imnan  690  jaoian  795  jaodan  797  stdcndc  845  impidc  858  pm2.5gdc  866  con2bidc  875  pm5.18dc  883  dfandc  884  pm4.63dc  886  pm4.54dc  902  pm4.79dc  903  orcanai  928  annimdc  937  pm4.55dc  938  orandc  939  pm4.82  950  pm3.11dc  957  pm3.12dc  958  dn1dc  960  3jcad  1178  3expia  1205  3an1rs  1219  3imp1  1220  3imp2  1222  syl3anl2  1287  3jaoian  1305  3jaodan  1306  mp3anl1  1331  mp3anl2  1332  mp3anl3  1333  ecased  1349  xor3dc  1387  pm5.15dc  1389  xor2dc  1390  xornbidc  1391  xordc  1392  nbbndc  1394  biassdc  1395  bilukdc  1396  dfbi3dc  1397  pm5.24dc  1398  xordidc  1399  alanimi  1459  19.29  1620  equs4  1725  equsexd  1729  spimth  1735  equs5a  1794  ax11v2  1820  ax11b  1826  equs5or  1830  sb5rf  1852  equvin  1863  nfsb4t  2014  eu5  2073  mopick  2104  euexex  2111  2euswapdc  2117  exists2  2123  eqrdav  2176  dvelimdc  2340  nebidc  2427  pm13.18  2428  nelne1  2437  nelne2  2438  rspa  2525  ralrimdvv  2561  r19.21bi  2565  r19.26  2603  ralbi  2609  rexbi  2610  r19.29  2614  vtoclgft  2789  rspcva  2841  rspc2va  2857  elabgt  2880  eqeu  2909  mob2  2919  mob  2921  euind  2926  reu6  2928  reuind  2944  sbctt  3031  rspsbca  3048  sbcnestgf  3110  rspcsbela  3118  ssel2  3152  sselda  3157  sstr  3165  nssne1  3215  nssne2  3216  reuss2  3417  reupick  3421  reupick2  3423  reximdva0m  3440  ssn0  3467  disjel  3479  ssdisj  3481  absneu  3666  preqr1g  3768  prel12  3773  dfiun2g  3920  nbrne1  4024  nbrne2  4025  mpteq12f  4085  triun  4116  csbexga  4133  iinexgm  4156  prexg  4213  copsex2t  4247  swopo  4308  poirr  4309  potr  4310  pofun  4314  issod  4321  ordelss  4381  trssord  4382  limelon  4401  trsuc  4424  eusvnfb  4456  rabxfrd  4471  regexmidlem1  4534  nordeq  4545  suc11g  4558  nnsuc  4617  brrelex12  4666  vtoclr  4676  optocl  4704  relop  4779  brcogw  4798  breldmg  4835  elreldm  4855  riinint  4890  issref  5013  xpidtr  5021  trin2  5022  cnveqb  5086  funopg  5252  funssres  5260  fununi  5286  funimass2  5296  imain  5300  fnun  5324  fco  5383  opelf  5389  f0rn0  5412  f1oun  5483  fun11iun  5484  fv3  5540  ndmfvg  5548  fvelima  5569  fvopab3ig  5592  fvmptssdm  5602  fvmptf  5610  fvimacnv  5633  fmptco  5684  funfvima2  5751  funfvima3  5752  f1veqaeq  5772  f1ocnvfvrneq  5785  fliftfun  5799  isotr  5819  isoini  5821  isopolem  5825  isosolem  5827  moriotass  5861  acexmidlem2  5874  suppssfv  6081  suppssov1  6082  f1dmex  6119  releldm2  6188  f1o2ndf1  6231  poxp  6235  tposf2  6271  iunon  6287  smoel2  6306  tfrlem9  6322  tfrexlem  6337  tfr1onlembxssdm  6346  tfr1onlemres  6352  tfrcllembxssdm  6359  tfrcllemres  6365  tfrcl  6367  tfri3  6370  frecabcl  6402  sucinc2  6449  nnacom  6487  nnmcom  6492  nnsucsssuc  6495  nnsucuniel  6498  nntri2or2  6501  nnaordi  6511  nnmordi  6519  nnaordex  6531  nnm00  6533  ectocld  6603  iinerm  6609  th3qlem2  6640  elpm2r  6668  mapsncnv  6697  mptelixpg  6736  ixpsnf1o  6738  f1oen3g  6756  f1oeng  6759  en2d  6770  en3d  6771  dom2lem  6774  fundmen  6808  fundmeng  6809  unen  6818  xpdom2  6833  xpdom2g  6834  fopwdom  6838  nneneq  6859  phpm  6867  phpelm  6868  dif1enen  6882  fin0  6887  findcard  6890  diffifi  6896  ac6sfi  6900  onunsnss  6918  fiintim  6930  xpfi  6931  fidcenum  6957  sbthlem1  6958  sbthlemi3  6960  sbthlemi10  6967  elfir  6974  isotilem  7007  inflbti  7025  ordiso2  7036  eldju2ndl  7073  eldju2ndr  7074  updjudhf  7080  mkvprop  7158  carden2bex  7190  pm54.43  7191  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  exmidfodomrlemim  7202  ltmpig  7340  enq0sym  7433  addnq0mo  7448  mulnq0mo  7449  prarloclem3step  7497  prarloclem3  7498  genpml  7518  genpmu  7519  genprndl  7522  genprndu  7523  genpdisj  7524  distrlem1prl  7583  distrlem1pru  7584  distrlem4prl  7585  distrlem4pru  7586  distrlem5prl  7587  distrlem5pru  7588  ltsopr  7597  ltaddpr  7598  addcanprleml  7615  addcanprlemu  7616  recexprlemm  7625  recexprlemlol  7627  recexprlemupu  7629  aptiprleml  7640  aptiprlemu  7641  caucvgprlemnkj  7667  caucvgprlemnbj  7668  addsrmo  7744  mulsrmo  7745  srpospr  7784  caucvgsr  7803  axprecex  7881  mulgt0  8034  ltne  8044  cnegexlem1  8134  cnegexlem2  8135  negf1o  8341  addgt0  8407  addgegt0  8408  addgtge0  8409  addge0  8410  recexre  8537  mulge0  8578  recexap  8612  prodgt02  8812  prodge02  8814  ltmul12a  8819  mulgt1  8822  nndivtr  8963  addltmul  9157  elnnnn0b  9222  xnn0nnn0pnf  9254  elnnz  9265  zmulcl  9308  nn0n0n1ge2  9325  nn0lt2  9336  nn0le2is012  9337  uzind2  9367  nn0ind-raph  9372  eluzp1m1  9553  uz3m2nn  9575  supinfneg  9597  infsupneg  9598  infregelbex  9600  negm  9617  lbzbi  9618  qaddcl  9637  qmulcl  9639  qreccl  9644  elpq  9650  ledivge1le  9728  nn0ledivnn  9769  xrltne  9815  xrre  9822  xrre2  9823  xrre3  9824  ge0gtmnf  9825  xltnegi  9837  xnn0xadd0  9869  xnegdi  9870  xposdif  9884  xlesubadd  9885  iccsupr  9968  icoshft  9992  icoshftf1o  9993  fznlem  10043  fzen  10045  uzsubsubfz  10049  fzsuc2  10081  elfz1b  10092  elfz0ubfz0  10127  elfz0fzfz0  10128  fz0fzelfz0  10129  fz0fzdiffz0  10132  elfzmlbp  10134  difelfznle  10137  fzofzim  10190  eluzgtdifelfzo  10199  elfzodifsumelfzo  10203  elfzonlteqm1  10212  elfzom1p1elfzo  10216  ssfzo12bi  10227  subfzo0  10244  exbtwnzlemstep  10250  modqmuladdnn0  10370  modfzo0difsn  10397  addmodlteq  10400  frec2uzlt2d  10406  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  m1expcl2  10544  expge1  10559  leexp2r  10576  expubnd  10579  zesq  10641  expnlbnd  10647  nn0ltexp2  10691  nn0opthd  10704  faclbnd  10723  bcpasc  10748  hashprg  10790  seq3coll  10824  rexanuz  10999  rexuz3  11001  r19.29uz  11003  r19.2uz  11004  absnid  11084  leabs  11085  ltabs  11098  icodiamlt  11191  maxleast  11224  negfi  11238  climcn2  11319  climcau  11357  climcaucn  11361  sumdc  11368  fsum3cvg  11388  isumz  11399  fsumf1o  11400  fisumss  11402  isumss2  11403  fsumzcl2  11415  fsumsplit  11417  fsumsplitsnun  11429  sumsplitdc  11442  fsum2dlemstep  11444  telfsumo  11476  fsumparts  11480  fsumiun  11487  isumrpcl  11504  fproddccvg  11582  prod1dc  11596  prodssdc  11599  fprodssdc  11600  prodsnf  11602  fprodsplitdc  11606  fprod2dlemstep  11632  fprodmodd  11651  efexp  11692  efieq1re  11781  p1modz1  11803  dvds0lem  11810  dvds2ln  11833  dvdssub2  11844  dvdsadd2b  11849  dvdsabseq  11855  divconjdvds  11857  dvdsdivcl  11858  odd2np1  11880  oddge22np1  11888  opoe  11902  omoe  11903  opeo  11904  omeo  11905  m1expo  11907  nn0ehalf  11910  nn0o1gt2  11912  nno  11913  divalgb  11932  ndvdsadd  11938  zsupcllemex  11949  zssinfcl  11951  gcd0id  11982  gcdneg  11985  gcdaddm  11987  bezoutlemstep  12000  dfgcd2  12017  gcddiv  12022  dvdsmulgcd  12028  bezoutr  12035  bezoutr1  12036  uzwodc  12040  algfx  12054  lcmgcdlem  12079  lcmgcdeq  12085  coprmdvds  12094  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  isprm3  12120  dvdsnprmd  12127  prmgt1  12134  oddprmgt2  12136  isprm6  12149  cncongrprm  12159  phibndlem  12218  phimullem  12227  powm2modprm  12254  modprm0  12256  modprmn0modprm0  12258  prm23lt5  12265  pcneg  12326  pcprmpw2  12334  dvdsprmpweqnn  12337  dvdsprmpweqle  12338  pcaddlem  12340  fldivp1  12348  pcfac  12350  oddprmdvds  12354  prmunb  12362  ennnfone  12428  unct  12445  lidrididd  12806  sgrpass  12819  issubmnd  12848  mnd1id  12853  insubm  12877  dfgrp2  12907  grpid  12917  grpasscan1  12938  dfgrp3mlem  12973  dfgrp3me  12975  mulgnn0p1  12999  mulgaddcom  13012  mulginvcom  13013  mulgass  13025  mulgpropdg  13030  subginv  13046  issubg2m  13054  issubg4m  13058  grpissubg  13059  resgrpisgrp  13060  subgintm  13063  cmncom  13110  nzrunit  13334  issubrg2  13367  subrgintm  13369  lmodfopnelem1  13419  lmodfopnelem2  13420  lmodfopne  13421  dvdsrzring  13532  uniopn  13540  istopon  13552  fiinbas  13588  tg2  13599  tgcl  13603  0nnei  13692  tgrest  13708  tgcn  13747  cnpnei  13758  cncnp2m  13770  lmtopcnp  13789  tx2cn  13809  txcn  13814  cnmpt21  13830  isxmet2d  13887  metrest  14045  metcnpi3  14056  tgioo  14085  fsumcncntop  14095  elcncf1di  14105  climcncf  14110  cncfco  14117  suplociccreex  14141  cnplimcim  14175  cnlimci  14181  reeff1olem  14231  efltlemlt  14234  zabsle1  14439  lgslem3  14442  lgsmod  14466  lgsdir2lem5  14472  lgsdir2  14473  lgsne0  14478  lgsdirnn0  14487  2lgsoddprmlem2  14493  bj-charfun  14598  bj-charfunr  14601  bj-charfunbi  14602  bj-prexg  14702  peano5set  14731  bj-peano4  14746  bj-nn0suc  14755  bj-nn0sucALT  14769  bj-findis  14770  exmidsbthrlem  14809  trilpolemres  14829  trirec0  14831  nconstwlpolem  14851  neapmkv  14854