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  938  pm4.55dc  939  orandc  940  pm4.82  951  pm3.11dc  958  pm3.12dc  959  dn1dc  961  3jcad  1179  3expia  1206  3an1rs  1220  3imp1  1221  3imp2  1223  syl3anl2  1297  3jaoian  1315  3jaodan  1316  mp3anl1  1341  mp3anl2  1342  mp3anl3  1343  ecased  1359  xor3dc  1397  pm5.15dc  1399  xor2dc  1400  xornbidc  1401  xordc  1402  nbbndc  1404  biassdc  1405  bilukdc  1406  dfbi3dc  1407  pm5.24dc  1408  xordidc  1409  alanimi  1469  19.29  1630  equs4  1735  equsexd  1739  spimth  1745  equs5a  1804  ax11v2  1830  ax11b  1836  equs5or  1840  sb5rf  1862  equvin  1873  nfsb4t  2024  eu5  2083  mopick  2114  euexex  2121  2euswapdc  2127  exists2  2133  eqrdav  2186  dvelimdc  2350  nebidc  2437  pm13.18  2438  nelne1  2447  nelne2  2448  rspa  2535  ralrimdvv  2571  r19.21bi  2575  r19.26  2613  ralbi  2619  rexbi  2620  r19.29  2624  vtoclgft  2799  rspcva  2851  rspc2va  2867  elabgt  2890  eqeu  2919  mob2  2929  mob  2931  euind  2936  reu6  2938  reuind  2954  sbctt  3041  rspsbca  3058  sbcnestgf  3120  rspcsbela  3128  ssel2  3162  sselda  3167  sstr  3175  nssne1  3225  nssne2  3226  reuss2  3427  reupick  3431  reupick2  3433  reximdva0m  3450  ssn0  3477  disjel  3489  ssdisj  3491  absneu  3676  preqr1g  3778  prel12  3783  dfiun2g  3930  nbrne1  4034  nbrne2  4035  mpteq12f  4095  triun  4126  csbexga  4143  iinexgm  4166  prexg  4223  copsex2t  4257  swopo  4318  poirr  4319  potr  4320  pofun  4324  issod  4331  ordelss  4391  trssord  4392  limelon  4411  trsuc  4434  eusvnfb  4466  rabxfrd  4481  regexmidlem1  4544  nordeq  4555  suc11g  4568  nnsuc  4627  brrelex12  4676  vtoclr  4686  optocl  4714  relop  4789  brcogw  4808  breldmg  4845  elreldm  4865  riinint  4900  issref  5023  xpidtr  5031  trin2  5032  cnveqb  5096  funopg  5262  funssres  5270  fununi  5296  funimass2  5306  imain  5310  fnun  5334  fco  5393  opelf  5399  f0rn0  5422  f1oun  5493  fun11iun  5494  fv3  5550  ndmfvg  5558  fvelima  5580  fvopab3ig  5603  fvmptssdm  5613  fvmptf  5621  fvimacnv  5644  fmptco  5695  funfvima2  5762  funfvima3  5763  f1veqaeq  5783  f1ocnvfvrneq  5796  fliftfun  5810  isotr  5830  isoini  5832  isopolem  5836  isosolem  5838  moriotass  5872  acexmidlem2  5885  suppssfv  6093  suppssov1  6094  f1dmex  6131  releldm2  6200  f1o2ndf1  6243  poxp  6247  tposf2  6283  iunon  6299  smoel2  6318  tfrlem9  6334  tfrexlem  6349  tfr1onlembxssdm  6358  tfr1onlemres  6364  tfrcllembxssdm  6371  tfrcllemres  6377  tfrcl  6379  tfri3  6382  frecabcl  6414  sucinc2  6461  nnacom  6499  nnmcom  6504  nnsucsssuc  6507  nnsucuniel  6510  nntri2or2  6513  nnaordi  6523  nnmordi  6531  nnaordex  6543  nnm00  6545  ectocld  6615  iinerm  6621  th3qlem2  6652  elpm2r  6680  mapsncnv  6709  mptelixpg  6748  ixpsnf1o  6750  f1oen3g  6768  f1oeng  6771  en2d  6782  en3d  6783  dom2lem  6786  fundmen  6820  fundmeng  6821  unen  6830  xpdom2  6845  xpdom2g  6846  fopwdom  6850  nneneq  6871  phpm  6879  phpelm  6880  dif1enen  6894  fin0  6899  findcard  6902  diffifi  6908  ac6sfi  6912  onunsnss  6930  fiintim  6942  xpfi  6943  fidcenum  6969  sbthlem1  6970  sbthlemi3  6972  sbthlemi10  6979  elfir  6986  isotilem  7019  inflbti  7037  ordiso2  7048  eldju2ndl  7085  eldju2ndr  7086  updjudhf  7092  mkvprop  7170  carden2bex  7202  pm54.43  7203  exmidfodomrlemeldju  7212  exmidfodomrlemreseldju  7213  exmidfodomrlemim  7214  ltmpig  7352  enq0sym  7445  addnq0mo  7460  mulnq0mo  7461  prarloclem3step  7509  prarloclem3  7510  genpml  7530  genpmu  7531  genprndl  7534  genprndu  7535  genpdisj  7536  distrlem1prl  7595  distrlem1pru  7596  distrlem4prl  7597  distrlem4pru  7598  distrlem5prl  7599  distrlem5pru  7600  ltsopr  7609  ltaddpr  7610  addcanprleml  7627  addcanprlemu  7628  recexprlemm  7637  recexprlemlol  7639  recexprlemupu  7641  aptiprleml  7652  aptiprlemu  7653  caucvgprlemnkj  7679  caucvgprlemnbj  7680  addsrmo  7756  mulsrmo  7757  srpospr  7796  caucvgsr  7815  axprecex  7893  mulgt0  8046  ltne  8056  cnegexlem1  8146  cnegexlem2  8147  negf1o  8353  addgt0  8419  addgegt0  8420  addgtge0  8421  addge0  8422  recexre  8549  mulge0  8590  recexap  8624  prodgt02  8824  prodge02  8826  ltmul12a  8831  mulgt1  8834  nndivtr  8975  addltmul  9169  elnnnn0b  9234  xnn0nnn0pnf  9266  elnnz  9277  zmulcl  9320  nn0n0n1ge2  9337  nn0lt2  9348  nn0le2is012  9349  uzind2  9379  nn0ind-raph  9384  eluzp1m1  9565  uz3m2nn  9587  supinfneg  9609  infsupneg  9610  infregelbex  9612  negm  9629  lbzbi  9630  qaddcl  9649  qmulcl  9651  qreccl  9656  elpq  9662  ledivge1le  9740  nn0ledivnn  9781  xrltne  9827  xrre  9834  xrre2  9835  xrre3  9836  ge0gtmnf  9837  xltnegi  9849  xnn0xadd0  9881  xnegdi  9882  xposdif  9896  xlesubadd  9897  iccsupr  9980  icoshft  10004  icoshftf1o  10005  fznlem  10055  fzen  10057  uzsubsubfz  10061  fzsuc2  10093  elfz1b  10104  elfz0ubfz0  10139  elfz0fzfz0  10140  fz0fzelfz0  10141  fz0fzdiffz0  10144  elfzmlbp  10146  difelfznle  10149  fzofzim  10202  eluzgtdifelfzo  10211  elfzodifsumelfzo  10215  elfzonlteqm1  10224  elfzom1p1elfzo  10228  ssfzo12bi  10239  subfzo0  10256  exbtwnzlemstep  10262  modqmuladdnn0  10382  modfzo0difsn  10409  addmodlteq  10412  frec2uzlt2d  10418  frecuzrdgtcl  10426  frecuzrdgfunlem  10433  m1expcl2  10556  expge1  10571  leexp2r  10588  expubnd  10591  zesq  10653  expnlbnd  10659  nn0ltexp2  10703  nn0opthd  10716  faclbnd  10735  bcpasc  10760  hashprg  10802  seq3coll  10836  rexanuz  11011  rexuz3  11013  r19.29uz  11015  r19.2uz  11016  absnid  11096  leabs  11097  ltabs  11110  icodiamlt  11203  maxleast  11236  negfi  11250  climcn2  11331  climcau  11369  climcaucn  11373  sumdc  11380  fsum3cvg  11400  isumz  11411  fsumf1o  11412  fisumss  11414  isumss2  11415  fsumzcl2  11427  fsumsplit  11429  fsumsplitsnun  11441  sumsplitdc  11454  fsum2dlemstep  11456  telfsumo  11488  fsumparts  11492  fsumiun  11499  isumrpcl  11516  fproddccvg  11594  prod1dc  11608  prodssdc  11611  fprodssdc  11612  prodsnf  11614  fprodsplitdc  11618  fprod2dlemstep  11644  fprodmodd  11663  efexp  11704  efieq1re  11793  p1modz1  11815  dvds0lem  11822  dvds2ln  11845  dvdssub2  11856  dvdsadd2b  11861  dvdsabseq  11867  divconjdvds  11869  dvdsdivcl  11870  odd2np1  11892  oddge22np1  11900  opoe  11914  omoe  11915  opeo  11916  omeo  11917  m1expo  11919  nn0ehalf  11922  nn0o1gt2  11924  nno  11925  divalgb  11944  ndvdsadd  11950  zsupcllemex  11961  zssinfcl  11963  gcd0id  11994  gcdneg  11997  gcdaddm  11999  bezoutlemstep  12012  dfgcd2  12029  gcddiv  12034  dvdsmulgcd  12040  bezoutr  12047  bezoutr1  12048  uzwodc  12052  algfx  12066  lcmgcdlem  12091  lcmgcdeq  12097  coprmdvds  12106  divgcdcoprmex  12116  cncongr1  12117  cncongr2  12118  isprm3  12132  dvdsnprmd  12139  prmgt1  12146  oddprmgt2  12148  isprm6  12161  cncongrprm  12171  phibndlem  12230  phimullem  12239  powm2modprm  12266  modprm0  12268  modprmn0modprm0  12270  prm23lt5  12277  pcneg  12338  pcprmpw2  12346  dvdsprmpweqnn  12349  dvdsprmpweqle  12350  pcaddlem  12352  fldivp1  12360  pcfac  12362  oddprmdvds  12366  prmunb  12374  ennnfone  12440  unct  12457  lidrididd  12820  sgrpass  12833  issgrpd  12837  issubmnd  12865  mnd1id  12870  insubm  12894  dfgrp2  12924  grpid  12936  grpasscan1  12960  dfgrp3mlem  12995  dfgrp3me  12997  imasgrp2  13005  mulgnn0p1  13026  mulgaddcom  13039  mulginvcom  13040  mulgass  13052  mulgpropdg  13057  subginv  13073  issubg2m  13081  issubg4m  13085  grpissubg  13086  resgrpisgrp  13087  subgintm  13090  cmncom  13139  imasabl  13171  rngdi  13192  rngdir  13193  rngpropd  13207  imasrng  13208  imasring  13312  nzrunit  13408  issubrng2  13430  subrngintm  13432  issubrg2  13461  subrgintm  13463  lmodfopnelem1  13513  lmodfopnelem2  13514  lmodfopne  13515  islssm  13546  islidlm  13668  rnglidlmcl  13669  dflidl2rng  13670  rnglidlmmgm  13685  rnglidlmsgrp  13686  rnglidlrng  13687  dvdsrzring  13775  uniopn  13797  istopon  13809  fiinbas  13845  tg2  13856  tgcl  13860  0nnei  13949  tgrest  13965  tgcn  14004  cnpnei  14015  cncnp2m  14027  lmtopcnp  14046  tx2cn  14066  txcn  14071  cnmpt21  14087  isxmet2d  14144  metrest  14302  metcnpi3  14313  tgioo  14342  fsumcncntop  14352  elcncf1di  14362  climcncf  14367  cncfco  14374  suplociccreex  14398  cnplimcim  14432  cnlimci  14438  reeff1olem  14488  efltlemlt  14491  zabsle1  14696  lgslem3  14699  lgsmod  14723  lgsdir2lem5  14729  lgsdir2  14730  lgsne0  14735  lgsdirnn0  14744  2lgsoddprmlem2  14750  bj-charfun  14855  bj-charfunr  14858  bj-charfunbi  14859  bj-prexg  14959  peano5set  14988  bj-peano4  15003  bj-nn0suc  15012  bj-nn0sucALT  15026  bj-findis  15027  exmidsbthrlem  15067  trilpolemres  15087  trirec0  15089  nconstwlpolem  15110  neapmkv  15113