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  7268  pm54.43  7269  exmidfodomrlemeldju  7278  exmidfodomrlemreseldju  7279  exmidfodomrlemim  7280  ltmpig  7423  enq0sym  7516  addnq0mo  7531  mulnq0mo  7532  prarloclem3step  7580  prarloclem3  7581  genpml  7601  genpmu  7602  genprndl  7605  genprndu  7606  genpdisj  7607  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  distrlem5prl  7670  distrlem5pru  7671  ltsopr  7680  ltaddpr  7681  addcanprleml  7698  addcanprlemu  7699  recexprlemm  7708  recexprlemlol  7710  recexprlemupu  7712  aptiprleml  7723  aptiprlemu  7724  caucvgprlemnkj  7750  caucvgprlemnbj  7751  addsrmo  7827  mulsrmo  7828  srpospr  7867  caucvgsr  7886  axprecex  7964  mpomulf  8033  mulgt0  8118  ltne  8128  cnegexlem1  8218  cnegexlem2  8219  negf1o  8425  addgt0  8492  addgegt0  8493  addgtge0  8494  addge0  8495  recexre  8622  mulge0  8663  recexap  8697  prodgt02  8897  prodge02  8899  ltmul12a  8904  mulgt1  8907  nndivtr  9049  addltmul  9245  elnnnn0b  9310  xnn0nnn0pnf  9342  elnnz  9353  zmulcl  9396  nn0n0n1ge2  9413  nn0lt2  9424  nn0le2is012  9425  uzind2  9455  nn0ind-raph  9460  eluzp1m1  9642  uz3m2nn  9664  supinfneg  9686  infsupneg  9687  infregelbex  9689  negm  9706  lbzbi  9707  qaddcl  9726  qmulcl  9728  qreccl  9733  elpq  9740  ledivge1le  9818  nn0ledivnn  9859  xrltne  9905  xrre  9912  xrre2  9913  xrre3  9914  ge0gtmnf  9915  xltnegi  9927  xnn0xadd0  9959  xnegdi  9960  xposdif  9974  xlesubadd  9975  iccsupr  10058  icoshft  10082  icoshftf1o  10083  fznlem  10133  fzen  10135  uzsubsubfz  10139  fzsuc2  10171  elfz1b  10182  elfz0ubfz0  10217  elfz0fzfz0  10218  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzmlbp  10224  difelfznle  10227  fzofzim  10281  eluzgtdifelfzo  10290  elfzodifsumelfzo  10294  elfzonlteqm1  10303  elfzom1p1elfzo  10307  ssfzo12bi  10318  subfzo0  10335  zsupcllemex  10337  zssinfcl  10339  exbtwnzlemstep  10354  modqmuladdnn0  10477  modfzo0difsn  10504  addmodlteq  10507  frec2uzlt2d  10513  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seqf1og  10630  m1expcl2  10670  expge1  10685  leexp2r  10702  expubnd  10705  zesq  10767  expnlbnd  10773  nn0ltexp2  10818  nn0opthd  10831  faclbnd  10850  bcpasc  10875  hashprg  10917  seq3coll  10951  wrdnval  10982  wrdsymb0  10984  fstwrdne  10990  wrdred1hash  10995  rexanuz  11170  rexuz3  11172  r19.29uz  11174  r19.2uz  11175  absnid  11255  leabs  11256  ltabs  11269  icodiamlt  11362  maxleast  11395  negfi  11410  climcn2  11491  climcau  11529  climcaucn  11533  sumdc  11540  fsum3cvg  11560  isumz  11571  fsumf1o  11572  fisumss  11574  isumss2  11575  fsumzcl2  11587  fsumsplit  11589  fsumsplitsnun  11601  sumsplitdc  11614  fsum2dlemstep  11616  telfsumo  11648  fsumparts  11652  fsumiun  11659  isumrpcl  11676  fproddccvg  11754  prod1dc  11768  prodssdc  11771  fprodssdc  11772  prodsnf  11774  fprodsplitdc  11778  fprod2dlemstep  11804  fprodmodd  11823  efexp  11864  efieq1re  11954  p1modz1  11976  dvds0lem  11983  dvds2ln  12006  dvdssub2  12017  dvdsadd2b  12022  dvdsabseq  12029  divconjdvds  12031  dvdsdivcl  12032  odd2np1  12055  oddge22np1  12063  opoe  12077  omoe  12078  opeo  12079  omeo  12080  m1expo  12082  nn0ehalf  12085  nn0o1gt2  12087  nno  12088  divalgb  12107  ndvdsadd  12113  bitsinv1lem  12143  gcd0id  12171  gcdneg  12174  gcdaddm  12176  bezoutlemstep  12189  dfgcd2  12206  gcddiv  12211  dvdsmulgcd  12217  bezoutr  12224  bezoutr1  12225  uzwodc  12229  nninfctlemfo  12232  algfx  12245  lcmgcdlem  12270  lcmgcdeq  12276  coprmdvds  12285  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  isprm3  12311  dvdsnprmd  12318  prmgt1  12325  oddprmgt2  12327  isprm6  12340  cncongrprm  12350  phibndlem  12409  phimullem  12418  powm2modprm  12446  modprm0  12448  modprmn0modprm0  12450  prm23lt5  12457  pcneg  12519  pcprmpw2  12527  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  pcaddlem  12533  fldivp1  12542  pcfac  12544  oddprmdvds  12548  prmunb  12556  ennnfone  12667  unct  12684  lidrididd  13084  gsummgmpropd  13096  sgrpass  13110  issgrpd  13114  issubmnd  13144  imasmnd2  13154  mnd1id  13158  insubm  13187  dfgrp2  13229  grpid  13241  grpasscan1  13265  dfgrp3mlem  13300  dfgrp3me  13302  imasgrp2  13316  mulgnn0gsum  13334  mulgnn0p1  13339  mulgaddcom  13352  mulginvcom  13353  mulgass  13365  mulgpropdg  13370  subginv  13387  issubg2m  13395  issubg4m  13399  grpissubg  13400  resgrpisgrp  13401  subgintm  13404  kerf1ghm  13480  cmncom  13508  imasabl  13542  rngdi  13572  rngdir  13573  rngpropd  13587  imasrng  13588  imasring  13696  nzrunit  13820  issubrng2  13842  subrngintm  13844  issubrg2  13873  subrgintm  13875  lmodfopnelem1  13956  lmodfopnelem2  13957  lmodfopne  13958  islssm  13989  islidlm  14111  rnglidlmcl  14112  dflidl2rng  14113  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  dvdsrzring  14235  znidom  14289  uniopn  14321  istopon  14333  fiinbas  14369  tg2  14380  tgcl  14384  0nnei  14473  tgrest  14489  tgcn  14528  cnpnei  14539  cncnp2m  14551  lmtopcnp  14570  tx2cn  14590  txcn  14595  cnmpt21  14611  isxmet2d  14668  metrest  14826  metcnpi3  14837  tgioo  14874  fsumcncntop  14887  elcncf1di  14899  climcncf  14904  cncfco  14911  suplociccreex  14944  cnplimcim  14987  cnlimci  14993  reeff1olem  15091  efltlemlt  15094  zabsle1  15324  lgslem3  15327  lgsmod  15351  lgsdir2lem5  15357  lgsdir2  15358  lgsne0  15363  lgsdirnn0  15372  gausslemma2dlem0f  15379  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  2lgslem1c  15415  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2lgslem3  15426  2lgsoddprmlem2  15431  bj-charfun  15537  bj-charfunr  15540  bj-charfunbi  15541  bj-prexg  15641  peano5set  15670  bj-peano4  15685  bj-nn0suc  15694  bj-nn0sucALT  15708  bj-findis  15709  exmidsbthrlem  15753  trilpolemres  15773  trirec0  15775  nconstwlpolem  15796  neapmkv  15799