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  688  imnan  692  jaoian  797  jaodan  799  stdcndc  847  impidc  860  pm2.5gdc  868  con2bidc  877  pm5.18dc  885  dfandc  886  pm4.63dc  888  pm4.54dc  904  pm4.79dc  905  orcanai  930  annimdc  940  pm4.55dc  941  orandc  942  pm4.82  953  pm3.11dc  960  pm3.12dc  961  dn1dc  963  3jcad  1181  3expia  1208  3an1rs  1222  3imp1  1223  3imp2  1225  syl3anl2  1299  3jaoian  1318  3jaodan  1319  mp3anl1  1344  mp3anl2  1345  mp3anl3  1346  ecased  1362  xor3dc  1407  pm5.15dc  1409  xor2dc  1410  xornbidc  1411  xordc  1412  nbbndc  1414  biassdc  1415  bilukdc  1416  dfbi3dc  1417  pm5.24dc  1418  xordidc  1419  alanimi  1483  19.29  1644  equs4  1749  equsexd  1753  spimth  1759  equs5a  1818  ax11v2  1844  ax11b  1850  equs5or  1854  sb5rf  1876  equvin  1887  nfsb4t  2043  eu5  2102  mopick  2133  euexex  2140  2euswapdc  2146  exists2  2152  eqrdav  2205  dvelimdc  2370  nebidc  2457  pm13.18  2458  nelne1  2467  nelne2  2468  rspa  2555  ralrimdvv  2591  r19.21bi  2595  r19.26  2633  ralbi  2639  rexbi  2640  r19.29  2644  vtoclgft  2824  rspcva  2876  rspc2va  2892  elabgt  2915  eqeu  2944  mob2  2954  mob  2956  euind  2961  reu6  2963  reuind  2979  sbctt  3066  rspsbca  3083  sbcnestgf  3146  rspcsbela  3154  ssel2  3189  sselda  3194  sstr  3202  nssne1  3252  nssne2  3253  reuss2  3454  reupick  3458  reupick2  3460  reximdva0m  3477  ssn0  3504  disjel  3516  ssdisj  3518  absneu  3706  preqr1g  3809  prel12  3814  dfiun2g  3961  nbrne1  4066  nbrne2  4067  mpteq12f  4128  triun  4159  csbexga  4176  iinexgm  4202  prexg  4259  copsex2t  4293  swopo  4357  poirr  4358  potr  4359  pofun  4363  issod  4370  ordelss  4430  trssord  4431  limelon  4450  trsuc  4473  eusvnfb  4505  rabxfrd  4520  regexmidlem1  4585  nordeq  4596  suc11g  4609  nnsuc  4668  brrelex12  4717  vtoclr  4727  optocl  4755  relop  4832  brcogw  4851  breldmg  4889  elreldm  4909  riinint  4944  issref  5070  xpidtr  5078  trin2  5079  cnveqb  5143  funopg  5310  funssres  5318  fununi  5347  funimass2  5357  imain  5361  fnun  5387  fco  5447  opelf  5453  f0rn0  5477  f1oun  5549  fun11iun  5550  fv3  5606  ndmfvg  5614  fvelima  5637  fvopab3ig  5660  fvmptssdm  5671  fvmptf  5679  fvimacnv  5702  fmptco  5753  funfvima2  5824  funfvima3  5825  f1veqaeq  5845  f1ocnvfvrneq  5858  fliftfun  5872  isotr  5892  isoini  5894  isopolem  5898  isosolem  5900  moriotass  5935  acexmidlem2  5948  suppssfv  6161  suppssov1  6162  f1dmex  6208  releldm2  6278  f1o2ndf1  6321  poxp  6325  tposf2  6361  iunon  6377  smoel2  6396  tfrlem9  6412  tfrexlem  6427  tfr1onlembxssdm  6436  tfr1onlemres  6442  tfrcllembxssdm  6449  tfrcllemres  6455  tfrcl  6457  tfri3  6460  frecabcl  6492  sucinc2  6539  nnacom  6577  nnmcom  6582  nnsucsssuc  6585  nnsucuniel  6588  nntri2or2  6591  nnaordi  6601  nnmordi  6609  nnaordex  6621  nnm00  6623  ectocld  6695  iinerm  6701  th3qlem2  6732  elpm2r  6760  mapsncnv  6789  mptelixpg  6828  ixpsnf1o  6830  f1oen4g  6850  f1dom4g  6851  f1oen3g  6852  f1oeng  6855  en2d  6866  en3d  6867  dom2lem  6870  fundmen  6905  fundmeng  6906  unen  6915  rex2dom  6917  xpdom2  6933  xpdom2g  6934  fopwdom  6940  nneneq  6961  phpm  6969  phpelm  6970  dif1enen  6984  fin0  6989  findcard  6992  diffifi  6998  ac6sfi  7002  onunsnss  7021  fiintim  7035  xpfi  7036  infidc  7043  fidcenum  7065  sbthlem1  7066  sbthlemi3  7068  sbthlemi10  7075  elfir  7082  isotilem  7115  inflbti  7133  ordiso2  7144  eldju2ndl  7181  eldju2ndr  7182  updjudhf  7188  mkvprop  7267  carden2bex  7304  pm54.43  7305  exmidfodomrlemeldju  7314  exmidfodomrlemreseldju  7315  exmidfodomrlemim  7316  ltmpig  7459  enq0sym  7552  addnq0mo  7567  mulnq0mo  7568  prarloclem3step  7616  prarloclem3  7617  genpml  7637  genpmu  7638  genprndl  7641  genprndu  7642  genpdisj  7643  distrlem1prl  7702  distrlem1pru  7703  distrlem4prl  7704  distrlem4pru  7705  distrlem5prl  7706  distrlem5pru  7707  ltsopr  7716  ltaddpr  7717  addcanprleml  7734  addcanprlemu  7735  recexprlemm  7744  recexprlemlol  7746  recexprlemupu  7748  aptiprleml  7759  aptiprlemu  7760  caucvgprlemnkj  7786  caucvgprlemnbj  7787  addsrmo  7863  mulsrmo  7864  srpospr  7903  caucvgsr  7922  axprecex  8000  mpomulf  8069  mulgt0  8154  ltne  8164  cnegexlem1  8254  cnegexlem2  8255  negf1o  8461  addgt0  8528  addgegt0  8529  addgtge0  8530  addge0  8531  recexre  8658  mulge0  8699  recexap  8733  prodgt02  8933  prodge02  8935  ltmul12a  8940  mulgt1  8943  nndivtr  9085  addltmul  9281  elnnnn0b  9346  xnn0nnn0pnf  9378  elnnz  9389  zmulcl  9433  nn0n0n1ge2  9450  nn0lt2  9461  nn0le2is012  9462  uzind2  9492  nn0ind-raph  9497  eluzp1m1  9679  uz3m2nn  9701  supinfneg  9723  infsupneg  9724  infregelbex  9726  negm  9743  lbzbi  9744  qaddcl  9763  qmulcl  9765  qreccl  9770  elpq  9777  ledivge1le  9855  nn0ledivnn  9896  xrltne  9942  xrre  9949  xrre2  9950  xrre3  9951  ge0gtmnf  9952  xltnegi  9964  xnn0xadd0  9996  xnegdi  9997  xposdif  10011  xlesubadd  10012  iccsupr  10095  icoshft  10119  icoshftf1o  10120  fznlem  10170  fzen  10172  uzsubsubfz  10176  fzsuc2  10208  elfz1b  10219  elfz0ubfz0  10254  elfz0fzfz0  10255  fz0fzelfz0  10256  fz0fzdiffz0  10259  elfzmlbp  10261  difelfznle  10264  fzofzim  10319  elincfzoext  10329  eluzgtdifelfzo  10333  elfzodifsumelfzo  10337  elfzonlteqm1  10346  elfzom1p1elfzo  10350  ssfzo12bi  10361  subfzo0  10378  zsupcllemex  10380  zssinfcl  10382  exbtwnzlemstep  10397  modqmuladdnn0  10520  modfzo0difsn  10547  addmodlteq  10550  frec2uzlt2d  10556  frecuzrdgtcl  10564  frecuzrdgfunlem  10571  seqf1og  10673  m1expcl2  10713  expge1  10728  leexp2r  10745  expubnd  10748  zesq  10810  expnlbnd  10816  nn0ltexp2  10861  nn0opthd  10874  faclbnd  10893  bcpasc  10918  hashprg  10960  seq3coll  10994  wrdnval  11031  wrdsymb0  11033  fstwrdne  11039  wrdred1hash  11044  swrdnd  11120  swrdwrdsymbg  11125  swrdsbslen  11127  swrdlsw  11130  swrdswrdlem  11163  swrdswrd  11164  pfxswrd  11165  rexanuz  11343  rexuz3  11345  r19.29uz  11347  r19.2uz  11348  absnid  11428  leabs  11429  ltabs  11442  icodiamlt  11535  maxleast  11568  negfi  11583  climcn2  11664  climcau  11702  climcaucn  11706  sumdc  11713  fsum3cvg  11733  isumz  11744  fsumf1o  11745  fisumss  11747  isumss2  11748  fsumzcl2  11760  fsumsplit  11762  fsumsplitsnun  11774  sumsplitdc  11787  fsum2dlemstep  11789  telfsumo  11821  fsumparts  11825  fsumiun  11832  isumrpcl  11849  fproddccvg  11927  prod1dc  11941  prodssdc  11944  fprodssdc  11945  prodsnf  11947  fprodsplitdc  11951  fprod2dlemstep  11977  fprodmodd  11996  efexp  12037  efieq1re  12127  p1modz1  12149  dvds0lem  12156  dvds2ln  12179  dvdssub2  12190  dvdsadd2b  12195  dvdsabseq  12202  divconjdvds  12204  dvdsdivcl  12205  odd2np1  12228  oddge22np1  12236  opoe  12250  omoe  12251  opeo  12252  omeo  12253  m1expo  12255  nn0ehalf  12258  nn0o1gt2  12260  nno  12261  divalgb  12280  ndvdsadd  12286  bitsinv1lem  12316  gcd0id  12344  gcdneg  12347  gcdaddm  12349  bezoutlemstep  12362  dfgcd2  12379  gcddiv  12384  dvdsmulgcd  12390  bezoutr  12397  bezoutr1  12398  uzwodc  12402  nninfctlemfo  12405  algfx  12418  lcmgcdlem  12443  lcmgcdeq  12449  coprmdvds  12458  divgcdcoprmex  12468  cncongr1  12469  cncongr2  12470  isprm3  12484  dvdsnprmd  12491  prmgt1  12498  oddprmgt2  12500  isprm6  12513  cncongrprm  12523  phibndlem  12582  phimullem  12591  powm2modprm  12619  modprm0  12621  modprmn0modprm0  12623  prm23lt5  12630  pcneg  12692  pcprmpw2  12700  dvdsprmpweqnn  12703  dvdsprmpweqle  12704  pcaddlem  12706  fldivp1  12715  pcfac  12717  oddprmdvds  12721  prmunb  12729  ennnfone  12840  unct  12857  lidrididd  13258  gsummgmpropd  13270  sgrpass  13284  issgrpd  13288  issubmnd  13318  imasmnd2  13328  mnd1id  13332  insubm  13361  dfgrp2  13403  grpid  13415  grpasscan1  13439  dfgrp3mlem  13474  dfgrp3me  13476  imasgrp2  13490  mulgnn0gsum  13508  mulgnn0p1  13513  mulgaddcom  13526  mulginvcom  13527  mulgass  13539  mulgpropdg  13544  subginv  13561  issubg2m  13569  issubg4m  13573  grpissubg  13574  resgrpisgrp  13575  subgintm  13578  kerf1ghm  13654  cmncom  13682  imasabl  13716  rngdi  13746  rngdir  13747  rngpropd  13761  imasrng  13762  imasring  13870  nzrunit  13994  issubrng2  14016  subrngintm  14018  issubrg2  14047  subrgintm  14049  lmodfopnelem1  14130  lmodfopnelem2  14131  lmodfopne  14132  islssm  14163  islidlm  14285  rnglidlmcl  14286  dflidl2rng  14287  rnglidlmmgm  14302  rnglidlmsgrp  14303  rnglidlrng  14304  dvdsrzring  14409  znidom  14463  uniopn  14517  istopon  14529  fiinbas  14565  tg2  14576  tgcl  14580  0nnei  14669  tgrest  14685  tgcn  14724  cnpnei  14735  cncnp2m  14747  lmtopcnp  14766  tx2cn  14786  txcn  14791  cnmpt21  14807  isxmet2d  14864  metrest  15022  metcnpi3  15033  tgioo  15070  fsumcncntop  15083  elcncf1di  15095  climcncf  15100  cncfco  15107  suplociccreex  15140  cnplimcim  15183  cnlimci  15189  reeff1olem  15287  efltlemlt  15290  zabsle1  15520  lgslem3  15523  lgsmod  15547  lgsdir2lem5  15553  lgsdir2  15554  lgsne0  15559  lgsdirnn0  15568  gausslemma2dlem0f  15575  gausslemma2dlem1a  15579  gausslemma2dlem3  15584  2lgslem1c  15611  2lgslem3a1  15618  2lgslem3b1  15619  2lgslem3c1  15620  2lgslem3d1  15621  2lgslem3  15622  2lgsoddprmlem2  15627  uhgrm  15718  incistruhgr  15730  bj-charfun  15817  bj-charfunr  15820  bj-charfunbi  15821  bj-prexg  15921  peano5set  15950  bj-peano4  15965  bj-nn0suc  15974  bj-nn0sucALT  15988  bj-findis  15989  exmidsbthrlem  16035  trilpolemres  16055  trirec0  16057  nconstwlpolem  16078  neapmkv  16081