Theorem imp 123

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 108	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		simpr 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		imp.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	sylc 62	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  impcom  124  impd  252  imp31  254  imp32  255  expdimp  257  impancom  258  pm3.22  263  ancoms  266  adantr  274  impel  278  biimpa  294  biimpar  295  biimpac  296  biimparc  297  pm3.33  343  pm3.34  344  pm3.35  345  pm5.31  346  imp4b  348  imp41  351  imp42  352  imp43  353  imp44  354  imp45  355  imp5g  358  expr  373  impac  379  sylan9  407  sylan9r  408  imdistani  442  mpan10  466  adantl4r  509  adantl5r  517  adantl6r  518  a2and  548  anabsi5  569  anim12dan  590  pm3.43  592  con3dimp  625  annimim  676  imnan  680  jaoian  785  jaodan  787  stdcndc  831  impidc  844  pm2.5gdc  852  con2bidc  861  pm5.18dc  869  dfandc  870  pm4.63dc  872  pm4.54dc  888  pm4.79dc  889  orcanai  914  annimdc  922  pm4.55dc  923  orandc  924  pm4.82  935  pm3.11dc  942  pm3.12dc  943  dn1dc  945  3jcad  1163  3expia  1187  3an1rs  1201  3imp1  1202  3imp2  1204  syl3anl2  1269  3jaoian  1287  3jaodan  1288  mp3anl1  1313  mp3anl2  1314  mp3anl3  1315  ecased  1331  xor3dc  1369  pm5.15dc  1371  xor2dc  1372  xornbidc  1373  xordc  1374  nbbndc  1376  biassdc  1377  bilukdc  1378  dfbi3dc  1379  pm5.24dc  1380  xordidc  1381  alanimi  1439  19.29  1600  equs4  1705  equsexd  1709  spimth  1715  equs5a  1774  ax11v2  1800  ax11b  1806  equs5or  1810  sb5rf  1832  equvin  1843  nfsb4t  1994  eu5  2053  mopick  2084  euexex  2091  2euswapdc  2097  exists2  2103  eqrdav  2156  dvelimdc  2320  nebidc  2407  pm13.18  2408  nelne1  2417  nelne2  2418  rspa  2505  ralrimdvv  2541  r19.21bi  2545  r19.26  2583  ralbi  2589  rexbi  2590  r19.29  2594  vtoclgft  2762  rspcva  2814  rspc2va  2830  elabgt  2853  eqeu  2882  mob2  2892  mob  2894  euind  2899  reu6  2901  reuind  2917  sbctt  3003  rspsbca  3020  sbcnestgf  3082  rspcsbela  3090  ssel2  3123  sselda  3128  sstr  3136  nssne1  3186  nssne2  3187  reuss2  3387  reupick  3391  reupick2  3393  reximdva0m  3409  ssn0  3436  disjel  3448  ssdisj  3450  absneu  3631  preqr1g  3729  prel12  3734  dfiun2g  3881  nbrne1  3983  nbrne2  3984  mpteq12f  4044  triun  4075  csbexga  4092  iinexgm  4115  prexg  4171  copsex2t  4205  swopo  4266  poirr  4267  potr  4268  pofun  4272  issod  4279  ordelss  4339  trssord  4340  limelon  4359  trsuc  4382  eusvnfb  4413  rabxfrd  4428  regexmidlem1  4491  nordeq  4502  suc11g  4515  nnsuc  4574  brrelex12  4623  vtoclr  4633  optocl  4661  relop  4735  brcogw  4754  breldmg  4791  elreldm  4811  riinint  4846  issref  4967  xpidtr  4975  trin2  4976  cnveqb  5040  funopg  5203  funssres  5211  fununi  5237  funimass2  5247  imain  5251  fnun  5275  fco  5334  opelf  5340  f0rn0  5363  f1oun  5433  fun11iun  5434  fv3  5490  ndmfvg  5498  fvelima  5519  fvopab3ig  5541  fvmptssdm  5551  fvmptf  5559  fvimacnv  5581  fmptco  5632  funfvima2  5696  funfvima3  5697  f1veqaeq  5716  f1ocnvfvrneq  5729  fliftfun  5743  isotr  5763  isoini  5765  isopolem  5769  isosolem  5771  moriotass  5805  acexmidlem2  5818  suppssfv  6025  suppssov1  6026  f1dmex  6061  releldm2  6130  f1o2ndf1  6172  poxp  6176  tposf2  6212  iunon  6228  smoel2  6247  tfrlem9  6263  tfrexlem  6278  tfr1onlembxssdm  6287  tfr1onlemres  6293  tfrcllembxssdm  6300  tfrcllemres  6306  tfrcl  6308  tfri3  6311  frecabcl  6343  sucinc2  6390  nnacom  6428  nnmcom  6433  nnsucsssuc  6436  nnsucuniel  6439  nntri2or2  6442  nnaordi  6452  nnmordi  6460  nnaordex  6471  nnm00  6473  ectocld  6543  iinerm  6549  th3qlem2  6580  elpm2r  6608  mapsncnv  6637  mptelixpg  6676  ixpsnf1o  6678  f1oen3g  6696  f1oeng  6699  en2d  6710  en3d  6711  dom2lem  6714  fundmen  6748  fundmeng  6749  unen  6758  xpdom2  6773  xpdom2g  6774  fopwdom  6778  nneneq  6799  phpm  6807  phpelm  6808  dif1enen  6822  fin0  6827  findcard  6830  diffifi  6836  ac6sfi  6840  onunsnss  6858  fiintim  6870  xpfi  6871  fidcenum  6897  sbthlem1  6898  sbthlemi3  6900  sbthlemi10  6907  elfir  6914  isotilem  6946  inflbti  6964  ordiso2  6973  eldju2ndl  7010  eldju2ndr  7011  updjudhf  7017  mkvprop  7095  carden2bex  7118  pm54.43  7119  exmidfodomrlemeldju  7128  exmidfodomrlemreseldju  7129  exmidfodomrlemim  7130  ltmpig  7253  enq0sym  7346  addnq0mo  7361  mulnq0mo  7362  prarloclem3step  7410  prarloclem3  7411  genpml  7431  genpmu  7432  genprndl  7435  genprndu  7436  genpdisj  7437  distrlem1prl  7496  distrlem1pru  7497  distrlem4prl  7498  distrlem4pru  7499  distrlem5prl  7500  distrlem5pru  7501  ltsopr  7510  ltaddpr  7511  addcanprleml  7528  addcanprlemu  7529  recexprlemm  7538  recexprlemlol  7540  recexprlemupu  7542  aptiprleml  7553  aptiprlemu  7554  caucvgprlemnkj  7580  caucvgprlemnbj  7581  addsrmo  7657  mulsrmo  7658  srpospr  7697  caucvgsr  7716  axprecex  7794  mulgt0  7946  ltne  7956  cnegexlem1  8044  cnegexlem2  8045  negf1o  8251  addgt0  8317  addgegt0  8318  addgtge0  8319  addge0  8320  recexre  8447  mulge0  8488  recexap  8521  prodgt02  8718  prodge02  8720  ltmul12a  8725  mulgt1  8728  nndivtr  8869  addltmul  9063  elnnnn0b  9128  xnn0nnn0pnf  9160  elnnz  9171  zmulcl  9214  nn0n0n1ge2  9228  nn0lt2  9239  nn0le2is012  9240  uzind2  9270  nn0ind-raph  9275  eluzp1m1  9456  uz3m2nn  9478  supinfneg  9500  infsupneg  9501  negm  9517  lbzbi  9518  qaddcl  9537  qmulcl  9539  qreccl  9544  elpq  9550  ledivge1le  9626  nn0ledivnn  9667  xrltne  9710  xrre  9717  xrre2  9718  xrre3  9719  ge0gtmnf  9720  xltnegi  9732  xnn0xadd0  9764  xnegdi  9765  xposdif  9779  xlesubadd  9780  iccsupr  9863  icoshft  9887  icoshftf1o  9888  fznlem  9936  fzen  9938  uzsubsubfz  9942  fzsuc2  9974  elfz1b  9985  elfz0ubfz0  10017  elfz0fzfz0  10018  fz0fzelfz0  10019  fz0fzdiffz0  10022  elfzmlbp  10024  difelfznle  10027  fzofzim  10080  eluzgtdifelfzo  10089  elfzodifsumelfzo  10093  elfzonlteqm1  10102  elfzom1p1elfzo  10106  ssfzo12bi  10117  subfzo0  10134  exbtwnzlemstep  10140  modqmuladdnn0  10260  modfzo0difsn  10287  addmodlteq  10290  frec2uzlt2d  10296  frecuzrdgtcl  10304  frecuzrdgfunlem  10311  m1expcl2  10434  expge1  10449  leexp2r  10466  expubnd  10469  zesq  10529  expnlbnd  10535  nn0opthd  10589  faclbnd  10608  bcpasc  10633  hashprg  10675  seq3coll  10706  rexanuz  10881  rexuz3  10883  r19.29uz  10885  r19.2uz  10886  absnid  10966  leabs  10967  ltabs  10980  icodiamlt  11073  maxleast  11106  negfi  11120  climcn2  11199  climcau  11237  climcaucn  11241  sumdc  11248  fsum3cvg  11268  isumz  11279  fsumf1o  11280  fisumss  11282  isumss2  11283  fsumzcl2  11295  fsumsplit  11297  fsumsplitsnun  11309  sumsplitdc  11322  fsum2dlemstep  11324  telfsumo  11356  fsumparts  11360  fsumiun  11367  isumrpcl  11384  fproddccvg  11462  prod1dc  11476  prodssdc  11479  fprodssdc  11480  prodsnf  11482  fprodsplitdc  11486  fprod2dlemstep  11512  fprodmodd  11531  efexp  11572  efieq1re  11661  p1modz1  11683  dvds0lem  11689  dvds2ln  11712  dvdssub2  11721  dvdsadd2b  11726  dvdsabseq  11731  divconjdvds  11733  dvdsdivcl  11734  odd2np1  11756  oddge22np1  11764  opoe  11778  omoe  11779  opeo  11780  omeo  11781  m1expo  11783  nn0ehalf  11786  nn0o1gt2  11788  nno  11789  divalgb  11808  ndvdsadd  11814  zsupcllemex  11825  zssinfcl  11827  gcd0id  11854  gcdneg  11857  gcdaddm  11859  bezoutlemstep  11872  dfgcd2  11889  gcddiv  11894  dvdsmulgcd  11900  bezoutr  11907  bezoutr1  11908  algfx  11920  lcmgcdlem  11945  lcmgcdeq  11951  coprmdvds  11960  divgcdcoprmex  11970  cncongr1  11971  cncongr2  11972  isprm3  11986  dvdsnprmd  11993  prmgt1  11999  oddprmgt2  12001  isprm6  12012  cncongrprm  12022  phibndlem  12079  phimullem  12088  ennnfone  12137  unct  12154  uniopn  12370  istopon  12382  fiinbas  12418  tg2  12431  tgcl  12435  0nnei  12524  tgrest  12540  tgcn  12579  cnpnei  12590  cncnp2m  12602  lmtopcnp  12621  tx2cn  12641  txcn  12646  cnmpt21  12662  isxmet2d  12719  metrest  12877  metcnpi3  12888  tgioo  12917  fsumcncntop  12927  elcncf1di  12937  climcncf  12942  cncfco  12949  suplociccreex  12973  cnplimcim  13007  cnlimci  13013  reeff1olem  13063  efltlemlt  13066  bj-charfun  13353  bj-charfunr  13356  bj-charfunbi  13357  bj-prexg  13457  peano5set  13486  bj-peano4  13501  bj-nn0suc  13510  bj-nn0sucALT  13524  bj-findis  13525  exmidsbthrlem  13564  trilpolemres  13584  trirec0  13586  nconstwlpolem  13606  neapmkv  13609