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  636  annimim  687  imnan  691  jaoian  796  jaodan  798  stdcndc  846  impidc  859  pm2.5gdc  867  con2bidc  876  pm5.18dc  884  dfandc  885  pm4.63dc  887  pm4.54dc  903  pm4.79dc  904  orcanai  929  annimdc  939  pm4.55dc  940  orandc  941  pm4.82  952  pm3.11dc  959  pm3.12dc  960  dn1dc  962  3jcad  1180  3expia  1207  3an1rs  1221  3imp1  1222  3imp2  1224  syl3anl2  1298  3jaoian  1316  3jaodan  1317  mp3anl1  1342  mp3anl2  1343  mp3anl3  1344  ecased  1360  xor3dc  1398  pm5.15dc  1400  xor2dc  1401  xornbidc  1402  xordc  1403  nbbndc  1405  biassdc  1406  bilukdc  1407  dfbi3dc  1408  pm5.24dc  1409  xordidc  1410  alanimi  1473  19.29  1634  equs4  1739  equsexd  1743  spimth  1749  equs5a  1808  ax11v2  1834  ax11b  1840  equs5or  1844  sb5rf  1866  equvin  1877  nfsb4t  2033  eu5  2092  mopick  2123  euexex  2130  2euswapdc  2136  exists2  2142  eqrdav  2195  dvelimdc  2360  nebidc  2447  pm13.18  2448  nelne1  2457  nelne2  2458  rspa  2545  ralrimdvv  2581  r19.21bi  2585  r19.26  2623  ralbi  2629  rexbi  2630  r19.29  2634  vtoclgft  2814  rspcva  2866  rspc2va  2882  elabgt  2905  eqeu  2934  mob2  2944  mob  2946  euind  2951  reu6  2953  reuind  2969  sbctt  3056  rspsbca  3073  sbcnestgf  3136  rspcsbela  3144  ssel2  3179  sselda  3184  sstr  3192  nssne1  3242  nssne2  3243  reuss2  3444  reupick  3448  reupick2  3450  reximdva0m  3467  ssn0  3494  disjel  3506  ssdisj  3508  absneu  3695  preqr1g  3797  prel12  3802  dfiun2g  3949  nbrne1  4053  nbrne2  4054  mpteq12f  4114  triun  4145  csbexga  4162  iinexgm  4188  prexg  4245  copsex2t  4279  swopo  4342  poirr  4343  potr  4344  pofun  4348  issod  4355  ordelss  4415  trssord  4416  limelon  4435  trsuc  4458  eusvnfb  4490  rabxfrd  4505  regexmidlem1  4570  nordeq  4581  suc11g  4594  nnsuc  4653  brrelex12  4702  vtoclr  4712  optocl  4740  relop  4817  brcogw  4836  breldmg  4873  elreldm  4893  riinint  4928  issref  5053  xpidtr  5061  trin2  5062  cnveqb  5126  funopg  5293  funssres  5301  fununi  5327  funimass2  5337  imain  5341  fnun  5367  fco  5426  opelf  5432  f0rn0  5455  f1oun  5527  fun11iun  5528  fv3  5584  ndmfvg  5592  fvelima  5615  fvopab3ig  5638  fvmptssdm  5649  fvmptf  5657  fvimacnv  5680  fmptco  5731  funfvima2  5798  funfvima3  5799  f1veqaeq  5819  f1ocnvfvrneq  5832  fliftfun  5846  isotr  5866  isoini  5868  isopolem  5872  isosolem  5874  moriotass  5909  acexmidlem2  5922  suppssfv  6135  suppssov1  6136  f1dmex  6182  releldm2  6252  f1o2ndf1  6295  poxp  6299  tposf2  6335  iunon  6351  smoel2  6370  tfrlem9  6386  tfrexlem  6401  tfr1onlembxssdm  6410  tfr1onlemres  6416  tfrcllembxssdm  6423  tfrcllemres  6429  tfrcl  6431  tfri3  6434  frecabcl  6466  sucinc2  6513  nnacom  6551  nnmcom  6556  nnsucsssuc  6559  nnsucuniel  6562  nntri2or2  6565  nnaordi  6575  nnmordi  6583  nnaordex  6595  nnm00  6597  ectocld  6669  iinerm  6675  th3qlem2  6706  elpm2r  6734  mapsncnv  6763  mptelixpg  6802  ixpsnf1o  6804  f1oen3g  6822  f1oeng  6825  en2d  6836  en3d  6837  dom2lem  6840  fundmen  6874  fundmeng  6875  unen  6884  xpdom2  6899  xpdom2g  6900  fopwdom  6906  nneneq  6927  phpm  6935  phpelm  6936  dif1enen  6950  fin0  6955  findcard  6958  diffifi  6964  ac6sfi  6968  onunsnss  6987  fiintim  7001  xpfi  7002  infidc  7009  fidcenum  7031  sbthlem1  7032  sbthlemi3  7034  sbthlemi10  7041  elfir  7048  isotilem  7081  inflbti  7099  ordiso2  7110  eldju2ndl  7147  eldju2ndr  7148  updjudhf  7154  mkvprop  7233  carden2bex  7270  pm54.43  7271  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  exmidfodomrlemim  7282  ltmpig  7425  enq0sym  7518  addnq0mo  7533  mulnq0mo  7534  prarloclem3step  7582  prarloclem3  7583  genpml  7603  genpmu  7604  genprndl  7607  genprndu  7608  genpdisj  7609  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  distrlem5prl  7672  distrlem5pru  7673  ltsopr  7682  ltaddpr  7683  addcanprleml  7700  addcanprlemu  7701  recexprlemm  7710  recexprlemlol  7712  recexprlemupu  7714  aptiprleml  7725  aptiprlemu  7726  caucvgprlemnkj  7752  caucvgprlemnbj  7753  addsrmo  7829  mulsrmo  7830  srpospr  7869  caucvgsr  7888  axprecex  7966  mpomulf  8035  mulgt0  8120  ltne  8130  cnegexlem1  8220  cnegexlem2  8221  negf1o  8427  addgt0  8494  addgegt0  8495  addgtge0  8496  addge0  8497  recexre  8624  mulge0  8665  recexap  8699  prodgt02  8899  prodge02  8901  ltmul12a  8906  mulgt1  8909  nndivtr  9051  addltmul  9247  elnnnn0b  9312  xnn0nnn0pnf  9344  elnnz  9355  zmulcl  9398  nn0n0n1ge2  9415  nn0lt2  9426  nn0le2is012  9427  uzind2  9457  nn0ind-raph  9462  eluzp1m1  9644  uz3m2nn  9666  supinfneg  9688  infsupneg  9689  infregelbex  9691  negm  9708  lbzbi  9709  qaddcl  9728  qmulcl  9730  qreccl  9735  elpq  9742  ledivge1le  9820  nn0ledivnn  9861  xrltne  9907  xrre  9914  xrre2  9915  xrre3  9916  ge0gtmnf  9917  xltnegi  9929  xnn0xadd0  9961  xnegdi  9962  xposdif  9976  xlesubadd  9977  iccsupr  10060  icoshft  10084  icoshftf1o  10085  fznlem  10135  fzen  10137  uzsubsubfz  10141  fzsuc2  10173  elfz1b  10184  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzmlbp  10226  difelfznle  10229  fzofzim  10283  eluzgtdifelfzo  10292  elfzodifsumelfzo  10296  elfzonlteqm1  10305  elfzom1p1elfzo  10309  ssfzo12bi  10320  subfzo0  10337  zsupcllemex  10339  zssinfcl  10341  exbtwnzlemstep  10356  modqmuladdnn0  10479  modfzo0difsn  10506  addmodlteq  10509  frec2uzlt2d  10515  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seqf1og  10632  m1expcl2  10672  expge1  10687  leexp2r  10704  expubnd  10707  zesq  10769  expnlbnd  10775  nn0ltexp2  10820  nn0opthd  10833  faclbnd  10852  bcpasc  10877  hashprg  10919  seq3coll  10953  wrdnval  10984  wrdsymb0  10986  fstwrdne  10992  wrdred1hash  10997  rexanuz  11172  rexuz3  11174  r19.29uz  11176  r19.2uz  11177  absnid  11257  leabs  11258  ltabs  11271  icodiamlt  11364  maxleast  11397  negfi  11412  climcn2  11493  climcau  11531  climcaucn  11535  sumdc  11542  fsum3cvg  11562  isumz  11573  fsumf1o  11574  fisumss  11576  isumss2  11577  fsumzcl2  11589  fsumsplit  11591  fsumsplitsnun  11603  sumsplitdc  11616  fsum2dlemstep  11618  telfsumo  11650  fsumparts  11654  fsumiun  11661  isumrpcl  11678  fproddccvg  11756  prod1dc  11770  prodssdc  11773  fprodssdc  11774  prodsnf  11776  fprodsplitdc  11780  fprod2dlemstep  11806  fprodmodd  11825  efexp  11866  efieq1re  11956  p1modz1  11978  dvds0lem  11985  dvds2ln  12008  dvdssub2  12019  dvdsadd2b  12024  dvdsabseq  12031  divconjdvds  12033  dvdsdivcl  12034  odd2np1  12057  oddge22np1  12065  opoe  12079  omoe  12080  opeo  12081  omeo  12082  m1expo  12084  nn0ehalf  12087  nn0o1gt2  12089  nno  12090  divalgb  12109  ndvdsadd  12115  bitsinv1lem  12145  gcd0id  12173  gcdneg  12176  gcdaddm  12178  bezoutlemstep  12191  dfgcd2  12208  gcddiv  12213  dvdsmulgcd  12219  bezoutr  12226  bezoutr1  12227  uzwodc  12231  nninfctlemfo  12234  algfx  12247  lcmgcdlem  12272  lcmgcdeq  12278  coprmdvds  12287  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  isprm3  12313  dvdsnprmd  12320  prmgt1  12327  oddprmgt2  12329  isprm6  12342  cncongrprm  12352  phibndlem  12411  phimullem  12420  powm2modprm  12448  modprm0  12450  modprmn0modprm0  12452  prm23lt5  12459  pcneg  12521  pcprmpw2  12529  dvdsprmpweqnn  12532  dvdsprmpweqle  12533  pcaddlem  12535  fldivp1  12544  pcfac  12546  oddprmdvds  12550  prmunb  12558  ennnfone  12669  unct  12686  lidrididd  13086  gsummgmpropd  13098  sgrpass  13112  issgrpd  13116  issubmnd  13146  imasmnd2  13156  mnd1id  13160  insubm  13189  dfgrp2  13231  grpid  13243  grpasscan1  13267  dfgrp3mlem  13302  dfgrp3me  13304  imasgrp2  13318  mulgnn0gsum  13336  mulgnn0p1  13341  mulgaddcom  13354  mulginvcom  13355  mulgass  13367  mulgpropdg  13372  subginv  13389  issubg2m  13397  issubg4m  13401  grpissubg  13402  resgrpisgrp  13403  subgintm  13406  kerf1ghm  13482  cmncom  13510  imasabl  13544  rngdi  13574  rngdir  13575  rngpropd  13589  imasrng  13590  imasring  13698  nzrunit  13822  issubrng2  13844  subrngintm  13846  issubrg2  13875  subrgintm  13877  lmodfopnelem1  13958  lmodfopnelem2  13959  lmodfopne  13960  islssm  13991  islidlm  14113  rnglidlmcl  14114  dflidl2rng  14115  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  dvdsrzring  14237  znidom  14291  uniopn  14345  istopon  14357  fiinbas  14393  tg2  14404  tgcl  14408  0nnei  14497  tgrest  14513  tgcn  14552  cnpnei  14563  cncnp2m  14575  lmtopcnp  14594  tx2cn  14614  txcn  14619  cnmpt21  14635  isxmet2d  14692  metrest  14850  metcnpi3  14861  tgioo  14898  fsumcncntop  14911  elcncf1di  14923  climcncf  14928  cncfco  14935  suplociccreex  14968  cnplimcim  15011  cnlimci  15017  reeff1olem  15115  efltlemlt  15118  zabsle1  15348  lgslem3  15351  lgsmod  15375  lgsdir2lem5  15381  lgsdir2  15382  lgsne0  15387  lgsdirnn0  15396  gausslemma2dlem0f  15403  gausslemma2dlem1a  15407  gausslemma2dlem3  15412  2lgslem1c  15439  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgslem3  15450  2lgsoddprmlem2  15455  bj-charfun  15561  bj-charfunr  15564  bj-charfunbi  15565  bj-prexg  15665  peano5set  15694  bj-peano4  15709  bj-nn0suc  15718  bj-nn0sucALT  15732  bj-findis  15733  exmidsbthrlem  15779  trilpolemres  15799  trirec0  15801  nconstwlpolem  15822  neapmkv  15825