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  1470  19.29  1631  equs4  1736  equsexd  1740  spimth  1746  equs5a  1805  ax11v2  1831  ax11b  1837  equs5or  1841  sb5rf  1863  equvin  1874  nfsb4t  2030  eu5  2089  mopick  2120  euexex  2127  2euswapdc  2133  exists2  2139  eqrdav  2192  dvelimdc  2357  nebidc  2444  pm13.18  2445  nelne1  2454  nelne2  2455  rspa  2542  ralrimdvv  2578  r19.21bi  2582  r19.26  2620  ralbi  2626  rexbi  2627  r19.29  2631  vtoclgft  2810  rspcva  2862  rspc2va  2878  elabgt  2901  eqeu  2930  mob2  2940  mob  2942  euind  2947  reu6  2949  reuind  2965  sbctt  3052  rspsbca  3069  sbcnestgf  3132  rspcsbela  3140  ssel2  3174  sselda  3179  sstr  3187  nssne1  3237  nssne2  3238  reuss2  3439  reupick  3443  reupick2  3445  reximdva0m  3462  ssn0  3489  disjel  3501  ssdisj  3503  absneu  3690  preqr1g  3792  prel12  3797  dfiun2g  3944  nbrne1  4048  nbrne2  4049  mpteq12f  4109  triun  4140  csbexga  4157  iinexgm  4183  prexg  4240  copsex2t  4274  swopo  4337  poirr  4338  potr  4339  pofun  4343  issod  4350  ordelss  4410  trssord  4411  limelon  4430  trsuc  4453  eusvnfb  4485  rabxfrd  4500  regexmidlem1  4565  nordeq  4576  suc11g  4589  nnsuc  4648  brrelex12  4697  vtoclr  4707  optocl  4735  relop  4812  brcogw  4831  breldmg  4868  elreldm  4888  riinint  4923  issref  5048  xpidtr  5056  trin2  5057  cnveqb  5121  funopg  5288  funssres  5296  fununi  5322  funimass2  5332  imain  5336  fnun  5360  fco  5419  opelf  5425  f0rn0  5448  f1oun  5520  fun11iun  5521  fv3  5577  ndmfvg  5585  fvelima  5608  fvopab3ig  5631  fvmptssdm  5642  fvmptf  5650  fvimacnv  5673  fmptco  5724  funfvima2  5791  funfvima3  5792  f1veqaeq  5812  f1ocnvfvrneq  5825  fliftfun  5839  isotr  5859  isoini  5861  isopolem  5865  isosolem  5867  moriotass  5902  acexmidlem2  5915  suppssfv  6126  suppssov1  6127  f1dmex  6168  releldm2  6238  f1o2ndf1  6281  poxp  6285  tposf2  6321  iunon  6337  smoel2  6356  tfrlem9  6372  tfrexlem  6387  tfr1onlembxssdm  6396  tfr1onlemres  6402  tfrcllembxssdm  6409  tfrcllemres  6415  tfrcl  6417  tfri3  6420  frecabcl  6452  sucinc2  6499  nnacom  6537  nnmcom  6542  nnsucsssuc  6545  nnsucuniel  6548  nntri2or2  6551  nnaordi  6561  nnmordi  6569  nnaordex  6581  nnm00  6583  ectocld  6655  iinerm  6661  th3qlem2  6692  elpm2r  6720  mapsncnv  6749  mptelixpg  6788  ixpsnf1o  6790  f1oen3g  6808  f1oeng  6811  en2d  6822  en3d  6823  dom2lem  6826  fundmen  6860  fundmeng  6861  unen  6870  xpdom2  6885  xpdom2g  6886  fopwdom  6892  nneneq  6913  phpm  6921  phpelm  6922  dif1enen  6936  fin0  6941  findcard  6944  diffifi  6950  ac6sfi  6954  onunsnss  6973  fiintim  6985  xpfi  6986  infidc  6993  fidcenum  7015  sbthlem1  7016  sbthlemi3  7018  sbthlemi10  7025  elfir  7032  isotilem  7065  inflbti  7083  ordiso2  7094  eldju2ndl  7131  eldju2ndr  7132  updjudhf  7138  mkvprop  7217  carden2bex  7249  pm54.43  7250  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemim  7261  ltmpig  7399  enq0sym  7492  addnq0mo  7507  mulnq0mo  7508  prarloclem3step  7556  prarloclem3  7557  genpml  7577  genpmu  7578  genprndl  7581  genprndu  7582  genpdisj  7583  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  distrlem5prl  7646  distrlem5pru  7647  ltsopr  7656  ltaddpr  7657  addcanprleml  7674  addcanprlemu  7675  recexprlemm  7684  recexprlemlol  7686  recexprlemupu  7688  aptiprleml  7699  aptiprlemu  7700  caucvgprlemnkj  7726  caucvgprlemnbj  7727  addsrmo  7803  mulsrmo  7804  srpospr  7843  caucvgsr  7862  axprecex  7940  mpomulf  8009  mulgt0  8094  ltne  8104  cnegexlem1  8194  cnegexlem2  8195  negf1o  8401  addgt0  8467  addgegt0  8468  addgtge0  8469  addge0  8470  recexre  8597  mulge0  8638  recexap  8672  prodgt02  8872  prodge02  8874  ltmul12a  8879  mulgt1  8882  nndivtr  9024  addltmul  9219  elnnnn0b  9284  xnn0nnn0pnf  9316  elnnz  9327  zmulcl  9370  nn0n0n1ge2  9387  nn0lt2  9398  nn0le2is012  9399  uzind2  9429  nn0ind-raph  9434  eluzp1m1  9616  uz3m2nn  9638  supinfneg  9660  infsupneg  9661  infregelbex  9663  negm  9680  lbzbi  9681  qaddcl  9700  qmulcl  9702  qreccl  9707  elpq  9714  ledivge1le  9792  nn0ledivnn  9833  xrltne  9879  xrre  9886  xrre2  9887  xrre3  9888  ge0gtmnf  9889  xltnegi  9901  xnn0xadd0  9933  xnegdi  9934  xposdif  9948  xlesubadd  9949  iccsupr  10032  icoshft  10056  icoshftf1o  10057  fznlem  10107  fzen  10109  uzsubsubfz  10113  fzsuc2  10145  elfz1b  10156  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzmlbp  10198  difelfznle  10201  fzofzim  10255  eluzgtdifelfzo  10264  elfzodifsumelfzo  10268  elfzonlteqm1  10277  elfzom1p1elfzo  10281  ssfzo12bi  10292  subfzo0  10309  exbtwnzlemstep  10316  modqmuladdnn0  10439  modfzo0difsn  10466  addmodlteq  10469  frec2uzlt2d  10475  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seqf1og  10592  m1expcl2  10632  expge1  10647  leexp2r  10664  expubnd  10667  zesq  10729  expnlbnd  10735  nn0ltexp2  10780  nn0opthd  10793  faclbnd  10812  bcpasc  10837  hashprg  10879  seq3coll  10913  wrdnval  10944  wrdsymb0  10946  fstwrdne  10952  wrdred1hash  10957  rexanuz  11132  rexuz3  11134  r19.29uz  11136  r19.2uz  11137  absnid  11217  leabs  11218  ltabs  11231  icodiamlt  11324  maxleast  11357  negfi  11371  climcn2  11452  climcau  11490  climcaucn  11494  sumdc  11501  fsum3cvg  11521  isumz  11532  fsumf1o  11533  fisumss  11535  isumss2  11536  fsumzcl2  11548  fsumsplit  11550  fsumsplitsnun  11562  sumsplitdc  11575  fsum2dlemstep  11577  telfsumo  11609  fsumparts  11613  fsumiun  11620  isumrpcl  11637  fproddccvg  11715  prod1dc  11729  prodssdc  11732  fprodssdc  11733  prodsnf  11735  fprodsplitdc  11739  fprod2dlemstep  11765  fprodmodd  11784  efexp  11825  efieq1re  11915  p1modz1  11937  dvds0lem  11944  dvds2ln  11967  dvdssub2  11978  dvdsadd2b  11983  dvdsabseq  11989  divconjdvds  11991  dvdsdivcl  11992  odd2np1  12014  oddge22np1  12022  opoe  12036  omoe  12037  opeo  12038  omeo  12039  m1expo  12041  nn0ehalf  12044  nn0o1gt2  12046  nno  12047  divalgb  12066  ndvdsadd  12072  zsupcllemex  12083  zssinfcl  12085  gcd0id  12116  gcdneg  12119  gcdaddm  12121  bezoutlemstep  12134  dfgcd2  12151  gcddiv  12156  dvdsmulgcd  12162  bezoutr  12169  bezoutr1  12170  uzwodc  12174  nninfctlemfo  12177  algfx  12190  lcmgcdlem  12215  lcmgcdeq  12221  coprmdvds  12230  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  isprm3  12256  dvdsnprmd  12263  prmgt1  12270  oddprmgt2  12272  isprm6  12285  cncongrprm  12295  phibndlem  12354  phimullem  12363  powm2modprm  12390  modprm0  12392  modprmn0modprm0  12394  prm23lt5  12401  pcneg  12463  pcprmpw2  12471  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  pcaddlem  12477  fldivp1  12486  pcfac  12488  oddprmdvds  12492  prmunb  12500  ennnfone  12582  unct  12599  lidrididd  12965  gsummgmpropd  12977  sgrpass  12991  issgrpd  12995  issubmnd  13023  mnd1id  13028  insubm  13057  dfgrp2  13099  grpid  13111  grpasscan1  13135  dfgrp3mlem  13170  dfgrp3me  13172  imasgrp2  13180  mulgnn0gsum  13198  mulgnn0p1  13203  mulgaddcom  13216  mulginvcom  13217  mulgass  13229  mulgpropdg  13234  subginv  13251  issubg2m  13259  issubg4m  13263  grpissubg  13264  resgrpisgrp  13265  subgintm  13268  kerf1ghm  13344  cmncom  13372  imasabl  13406  rngdi  13436  rngdir  13437  rngpropd  13451  imasrng  13452  imasring  13560  nzrunit  13684  issubrng2  13706  subrngintm  13708  issubrg2  13737  subrgintm  13739  lmodfopnelem1  13820  lmodfopnelem2  13821  lmodfopne  13822  islssm  13853  islidlm  13975  rnglidlmcl  13976  dflidl2rng  13977  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  dvdsrzring  14091  znidom  14145  uniopn  14169  istopon  14181  fiinbas  14217  tg2  14228  tgcl  14232  0nnei  14321  tgrest  14337  tgcn  14376  cnpnei  14387  cncnp2m  14399  lmtopcnp  14418  tx2cn  14438  txcn  14443  cnmpt21  14459  isxmet2d  14516  metrest  14674  metcnpi3  14685  tgioo  14714  fsumcncntop  14724  elcncf1di  14734  climcncf  14739  cncfco  14746  suplociccreex  14778  cnplimcim  14821  cnlimci  14827  reeff1olem  14906  efltlemlt  14909  zabsle1  15115  lgslem3  15118  lgsmod  15142  lgsdir2lem5  15148  lgsdir2  15149  lgsne0  15154  lgsdirnn0  15163  gausslemma2dlem0f  15170  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  2lgsoddprmlem2  15194  bj-charfun  15299  bj-charfunr  15302  bj-charfunbi  15303  bj-prexg  15403  peano5set  15432  bj-peano4  15447  bj-nn0suc  15456  bj-nn0sucALT  15470  bj-findis  15471  exmidsbthrlem  15512  trilpolemres  15532  trirec0  15534  nconstwlpolem  15555  neapmkv  15558