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  prcssprc  4225  iinexgm  4239  prexg  4296  copsex2t  4332  swopo  4398  poirr  4399  potr  4400  pofun  4404  issod  4411  ordelss  4471  trssord  4472  limelon  4491  trsuc  4514  eusvnfb  4546  rabxfrd  4561  regexmidlem1  4626  nordeq  4637  suc11g  4650  nnsuc  4709  brrelex12  4759  vtoclr  4769  optocl  4797  relop  4875  brcogw  4894  breldmg  4932  elreldm  4953  riinint  4988  issref  5114  xpidtr  5122  trin2  5123  cnveqb  5187  funopg  5355  funssres  5363  fununi  5392  funimass2  5402  imain  5406  fnun  5432  fco  5494  opelf  5501  f0rn0  5525  f1oun  5597  fun11iun  5598  fv3  5655  ndmfvg  5663  fvelima  5690  fvopab3ig  5713  fvmptssdm  5724  fvmptf  5732  fvimacnv  5755  fmptco  5806  fcof  5825  funfvima2  5879  funfvima3  5880  f1veqaeq  5902  f1ocnvfvrneq  5915  fliftfun  5929  isotr  5949  isoini  5951  isopolem  5955  isosolem  5957  moriotass  5994  acexmidlem2  6007  suppssfv  6223  suppssov1  6224  f1dmex  6270  releldm2  6340  f1o2ndf1  6385  poxp  6389  tposf2  6425  iunon  6441  smoel2  6460  tfrlem9  6476  tfrexlem  6491  tfr1onlembxssdm  6500  tfr1onlemres  6506  tfrcllembxssdm  6513  tfrcllemres  6519  tfrcl  6521  tfri3  6524  frecabcl  6556  sucinc2  6605  nnacom  6643  nnmcom  6648  nnsucsssuc  6651  nnsucuniel  6654  nntri2or2  6657  nnaordi  6667  nnmordi  6675  nnaordex  6687  nnm00  6689  ectocld  6761  iinerm  6767  th3qlem2  6798  elpm2r  6826  mapsncnv  6855  mptelixpg  6894  ixpsnf1o  6896  f1oen4g  6916  f1dom4g  6917  f1oen3g  6918  f1oeng  6921  en2d  6932  en3d  6933  dom2lem  6936  fundmen  6972  fundmeng  6973  unen  6982  rex2dom  6984  en2m  6987  xpdom2  7003  xpdom2g  7004  fopwdom  7010  nneneq  7031  phpm  7040  phpelm  7041  dif1enen  7055  fin0  7060  findcard  7063  diffifi  7069  ac6sfi  7073  onunsnss  7095  fiintim  7109  xpfi  7110  infidc  7117  fidcenum  7139  sbthlem1  7140  sbthlemi3  7142  sbthlemi10  7149  elfir  7156  isotilem  7189  inflbti  7207  ordiso2  7218  eldju2ndl  7255  eldju2ndr  7256  updjudhf  7262  mkvprop  7341  carden2bex  7378  pm54.43  7379  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  exmidfodomrlemim  7395  pw1m  7425  ltmpig  7542  enq0sym  7635  addnq0mo  7650  mulnq0mo  7651  prarloclem3step  7699  prarloclem3  7700  genpml  7720  genpmu  7721  genprndl  7724  genprndu  7725  genpdisj  7726  distrlem1prl  7785  distrlem1pru  7786  distrlem4prl  7787  distrlem4pru  7788  distrlem5prl  7789  distrlem5pru  7790  ltsopr  7799  ltaddpr  7800  addcanprleml  7817  addcanprlemu  7818  recexprlemm  7827  recexprlemlol  7829  recexprlemupu  7831  aptiprleml  7842  aptiprlemu  7843  caucvgprlemnkj  7869  caucvgprlemnbj  7870  addsrmo  7946  mulsrmo  7947  srpospr  7986  caucvgsr  8005  axprecex  8083  mpomulf  8152  mulgt0  8237  ltne  8247  cnegexlem1  8337  cnegexlem2  8338  negf1o  8544  addgt0  8611  addgegt0  8612  addgtge0  8613  addge0  8614  recexre  8741  mulge0  8782  recexap  8816  prodgt02  9016  prodge02  9018  ltmul12a  9023  mulgt1  9026  nndivtr  9168  addltmul  9364  elnnnn0b  9429  xnn0nnn0pnf  9461  elnnz  9472  zmulcl  9516  nn0n0n1ge2  9533  nn0lt2  9544  nn0le2is012  9545  uzind2  9575  nn0ind-raph  9580  eluzp1m1  9763  uz3m2nn  9785  supinfneg  9807  infsupneg  9808  infregelbex  9810  negm  9827  lbzbi  9828  qaddcl  9847  qmulcl  9849  qreccl  9854  elpq  9861  ledivge1le  9939  nn0ledivnn  9980  xrltne  10026  xrre  10033  xrre2  10034  xrre3  10035  ge0gtmnf  10036  xltnegi  10048  xnn0xadd0  10080  xnegdi  10081  xposdif  10095  xlesubadd  10096  iccsupr  10179  icoshft  10203  icoshftf1o  10204  fznlem  10254  fzen  10256  uzsubsubfz  10260  fzsuc2  10292  elfz1b  10303  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  elfzmlbp  10345  difelfznle  10348  fzofzim  10405  elincfzoext  10416  eluzgtdifelfzo  10420  elfzodifsumelfzo  10424  elfzonlteqm1  10433  elfzom1p1elfzo  10437  ssfzo12bi  10448  subfzo0  10465  zsupcllemex  10467  zssinfcl  10469  exbtwnzlemstep  10484  modqmuladdnn0  10607  modfzo0difsn  10634  addmodlteq  10637  frec2uzlt2d  10643  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  seqf1og  10760  m1expcl2  10800  expge1  10815  leexp2r  10832  expubnd  10835  zesq  10897  expnlbnd  10903  nn0ltexp2  10948  nn0opthd  10961  faclbnd  10980  bcpasc  11005  hashprg  11048  seq3coll  11082  wrdnval  11120  wrdsymb0  11122  fstwrdne  11128  wrdred1hash  11133  swrdnd  11212  swrdwrdsymbg  11217  swrdsbslen  11219  swrdlsw  11222  swrdswrdlem  11257  swrdswrd  11258  pfxswrd  11259  cats1un  11274  wrd2ind  11276  swrdccatin1  11278  pfxccatin12lem4  11279  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  swrdccatin2  11282  pfxccatin12lem2c  11283  pfxccatin12lem2  11284  pfxccatin12lem3  11285  pfxccatin12  11286  pfxccat3  11287  swrdccat  11288  pfxccat3a  11291  swrdccat3blem  11292  swrdccat3b  11293  swrdccatin2d  11297  reuccatpfxs1lem  11299  rexanuz  11520  rexuz3  11522  r19.29uz  11524  r19.2uz  11525  absnid  11605  leabs  11606  ltabs  11619  icodiamlt  11712  maxleast  11745  negfi  11760  climcn2  11841  climcau  11879  climcaucn  11883  sumdc  11890  fsum3cvg  11910  isumz  11921  fsumf1o  11922  fisumss  11924  isumss2  11925  fsumzcl2  11937  fsumsplit  11939  fsumsplitsnun  11951  sumsplitdc  11964  fsum2dlemstep  11966  telfsumo  11998  fsumparts  12002  fsumiun  12009  isumrpcl  12026  fproddccvg  12104  prod1dc  12118  prodssdc  12121  fprodssdc  12122  prodsnf  12124  fprodsplitdc  12128  fprod2dlemstep  12154  fprodmodd  12173  efexp  12214  efieq1re  12304  p1modz1  12326  dvds0lem  12333  dvds2ln  12356  dvdssub2  12367  dvdsadd2b  12372  dvdsabseq  12379  divconjdvds  12381  dvdsdivcl  12382  odd2np1  12405  oddge22np1  12413  opoe  12427  omoe  12428  opeo  12429  omeo  12430  m1expo  12432  nn0ehalf  12435  nn0o1gt2  12437  nno  12438  divalgb  12457  ndvdsadd  12463  bitsinv1lem  12493  gcd0id  12521  gcdneg  12524  gcdaddm  12526  bezoutlemstep  12539  dfgcd2  12556  gcddiv  12561  dvdsmulgcd  12567  bezoutr  12574  bezoutr1  12575  uzwodc  12579  nninfctlemfo  12582  algfx  12595  lcmgcdlem  12620  lcmgcdeq  12626  coprmdvds  12635  divgcdcoprmex  12645  cncongr1  12646  cncongr2  12647  isprm3  12661  dvdsnprmd  12668  prmgt1  12675  oddprmgt2  12677  isprm6  12690  cncongrprm  12700  phibndlem  12759  phimullem  12768  powm2modprm  12796  modprm0  12798  modprmn0modprm0  12800  prm23lt5  12807  pcneg  12869  pcprmpw2  12877  dvdsprmpweqnn  12880  dvdsprmpweqle  12881  pcaddlem  12883  fldivp1  12892  pcfac  12894  oddprmdvds  12898  prmunb  12906  ennnfone  13017  unct  13034  lidrididd  13436  gsummgmpropd  13448  sgrpass  13462  issgrpd  13466  issubmnd  13496  imasmnd2  13506  mnd1id  13510  insubm  13539  dfgrp2  13581  grpid  13593  grpasscan1  13617  dfgrp3mlem  13652  dfgrp3me  13654  imasgrp2  13668  mulgnn0gsum  13686  mulgnn0p1  13691  mulgaddcom  13704  mulginvcom  13705  mulgass  13717  mulgpropdg  13722  subginv  13739  issubg2m  13747  issubg4m  13751  grpissubg  13752  resgrpisgrp  13753  subgintm  13756  kerf1ghm  13832  cmncom  13860  imasabl  13894  rngdi  13924  rngdir  13925  rngpropd  13939  imasrng  13940  imasring  14048  nzrunit  14173  issubrng2  14195  subrngintm  14197  issubrg2  14226  subrgintm  14228  lmodfopnelem1  14309  lmodfopnelem2  14310  lmodfopne  14311  islssm  14342  islidlm  14464  rnglidlmcl  14465  dflidl2rng  14466  rnglidlmmgm  14481  rnglidlmsgrp  14482  rnglidlrng  14483  dvdsrzring  14588  znidom  14642  uniopn  14696  istopon  14708  fiinbas  14744  tg2  14755  tgcl  14759  0nnei  14848  tgrest  14864  tgcn  14903  cnpnei  14914  cncnp2m  14926  lmtopcnp  14945  tx2cn  14965  txcn  14970  cnmpt21  14986  isxmet2d  15043  metrest  15201  metcnpi3  15212  tgioo  15249  fsumcncntop  15262  elcncf1di  15274  climcncf  15279  cncfco  15286  suplociccreex  15319  cnplimcim  15362  cnlimci  15368  reeff1olem  15466  efltlemlt  15469  zabsle1  15699  lgslem3  15702  lgsmod  15726  lgsdir2lem5  15732  lgsdir2  15733  lgsne0  15738  lgsdirnn0  15747  gausslemma2dlem0f  15754  gausslemma2dlem1a  15758  gausslemma2dlem3  15763  2lgslem1c  15790  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  2lgslem3  15801  2lgsoddprmlem2  15806  uhgrm  15899  incistruhgr  15911  upgrfnen  15919  umgrfnen  15929  umgrnloop  15937  upgredgpr  15968  usgrausgrben  15991  usgredgop  15992  usgruspgrben  16005  usgrislfuspgrdom  16009  umgrvad2edg  16030  ushgredgedg  16045  ushgredgedgloop  16047  uhgr0v0e  16053  vtxdg0v  16080  wlkpropg  16096  wlkvg  16100  wlkl1loop  16130  upgriswlkdc  16132  upgrwlkedg  16133  upgrwlkvtxedg  16136  uspgr2wlkeq  16137  wlkres  16149  trlf1  16157  clwwlk1loop  16168  clwwlkccatlem  16169  isclwwlknx  16184  clwwlkn1loopb  16188  clwwlkext2edg  16190  umgr2cwwk2dif  16192  bj-charfun  16279  bj-charfunr  16282  bj-charfunbi  16283  bj-prexg  16383  peano5set  16412  bj-peano4  16427  bj-nn0suc  16436  bj-nn0sucALT  16450  bj-findis  16451  exmidsbthrlem  16504  trilpolemres  16524  trirec0  16526  nconstwlpolem  16547  neapmkv  16550