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  835  impidc  848  pm2.5gdc  856  con2bidc  865  pm5.18dc  873  dfandc  874  pm4.63dc  876  pm4.54dc  892  pm4.79dc  893  orcanai  918  annimdc  927  pm4.55dc  928  orandc  929  pm4.82  940  pm3.11dc  947  pm3.12dc  948  dn1dc  950  3jcad  1168  3expia  1195  3an1rs  1209  3imp1  1210  3imp2  1212  syl3anl2  1277  3jaoian  1295  3jaodan  1296  mp3anl1  1321  mp3anl2  1322  mp3anl3  1323  ecased  1339  xor3dc  1377  pm5.15dc  1379  xor2dc  1380  xornbidc  1381  xordc  1382  nbbndc  1384  biassdc  1385  bilukdc  1386  dfbi3dc  1387  pm5.24dc  1388  xordidc  1389  alanimi  1447  19.29  1608  equs4  1713  equsexd  1717  spimth  1723  equs5a  1782  ax11v2  1808  ax11b  1814  equs5or  1818  sb5rf  1840  equvin  1851  nfsb4t  2002  eu5  2061  mopick  2092  euexex  2099  2euswapdc  2105  exists2  2111  eqrdav  2164  dvelimdc  2328  nebidc  2415  pm13.18  2416  nelne1  2425  nelne2  2426  rspa  2513  ralrimdvv  2549  r19.21bi  2553  r19.26  2591  ralbi  2597  rexbi  2598  r19.29  2602  vtoclgft  2775  rspcva  2827  rspc2va  2843  elabgt  2866  eqeu  2895  mob2  2905  mob  2907  euind  2912  reu6  2914  reuind  2930  sbctt  3016  rspsbca  3033  sbcnestgf  3095  rspcsbela  3103  ssel2  3136  sselda  3141  sstr  3149  nssne1  3199  nssne2  3200  reuss2  3401  reupick  3405  reupick2  3407  reximdva0m  3423  ssn0  3450  disjel  3462  ssdisj  3464  absneu  3647  preqr1g  3745  prel12  3750  dfiun2g  3897  nbrne1  4000  nbrne2  4001  mpteq12f  4061  triun  4092  csbexga  4109  iinexgm  4132  prexg  4188  copsex2t  4222  swopo  4283  poirr  4284  potr  4285  pofun  4289  issod  4296  ordelss  4356  trssord  4357  limelon  4376  trsuc  4399  eusvnfb  4431  rabxfrd  4446  regexmidlem1  4509  nordeq  4520  suc11g  4533  nnsuc  4592  brrelex12  4641  vtoclr  4651  optocl  4679  relop  4753  brcogw  4772  breldmg  4809  elreldm  4829  riinint  4864  issref  4985  xpidtr  4993  trin2  4994  cnveqb  5058  funopg  5221  funssres  5229  fununi  5255  funimass2  5265  imain  5269  fnun  5293  fco  5352  opelf  5358  f0rn0  5381  f1oun  5451  fun11iun  5452  fv3  5508  ndmfvg  5516  fvelima  5537  fvopab3ig  5559  fvmptssdm  5569  fvmptf  5577  fvimacnv  5599  fmptco  5650  funfvima2  5716  funfvima3  5717  f1veqaeq  5736  f1ocnvfvrneq  5749  fliftfun  5763  isotr  5783  isoini  5785  isopolem  5789  isosolem  5791  moriotass  5825  acexmidlem2  5838  suppssfv  6045  suppssov1  6046  f1dmex  6081  releldm2  6150  f1o2ndf1  6192  poxp  6196  tposf2  6232  iunon  6248  smoel2  6267  tfrlem9  6283  tfrexlem  6298  tfr1onlembxssdm  6307  tfr1onlemres  6313  tfrcllembxssdm  6320  tfrcllemres  6326  tfrcl  6328  tfri3  6331  frecabcl  6363  sucinc2  6410  nnacom  6448  nnmcom  6453  nnsucsssuc  6456  nnsucuniel  6459  nntri2or2  6462  nnaordi  6472  nnmordi  6480  nnaordex  6491  nnm00  6493  ectocld  6563  iinerm  6569  th3qlem2  6600  elpm2r  6628  mapsncnv  6657  mptelixpg  6696  ixpsnf1o  6698  f1oen3g  6716  f1oeng  6719  en2d  6730  en3d  6731  dom2lem  6734  fundmen  6768  fundmeng  6769  unen  6778  xpdom2  6793  xpdom2g  6794  fopwdom  6798  nneneq  6819  phpm  6827  phpelm  6828  dif1enen  6842  fin0  6847  findcard  6850  diffifi  6856  ac6sfi  6860  onunsnss  6878  fiintim  6890  xpfi  6891  fidcenum  6917  sbthlem1  6918  sbthlemi3  6920  sbthlemi10  6927  elfir  6934  isotilem  6967  inflbti  6985  ordiso2  6996  eldju2ndl  7033  eldju2ndr  7034  updjudhf  7040  mkvprop  7118  carden2bex  7141  pm54.43  7142  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  exmidfodomrlemim  7153  ltmpig  7276  enq0sym  7369  addnq0mo  7384  mulnq0mo  7385  prarloclem3step  7433  prarloclem3  7434  genpml  7454  genpmu  7455  genprndl  7458  genprndu  7459  genpdisj  7460  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  distrlem5prl  7523  distrlem5pru  7524  ltsopr  7533  ltaddpr  7534  addcanprleml  7551  addcanprlemu  7552  recexprlemm  7561  recexprlemlol  7563  recexprlemupu  7565  aptiprleml  7576  aptiprlemu  7577  caucvgprlemnkj  7603  caucvgprlemnbj  7604  addsrmo  7680  mulsrmo  7681  srpospr  7720  caucvgsr  7739  axprecex  7817  mulgt0  7969  ltne  7979  cnegexlem1  8069  cnegexlem2  8070  negf1o  8276  addgt0  8342  addgegt0  8343  addgtge0  8344  addge0  8345  recexre  8472  mulge0  8513  recexap  8546  prodgt02  8744  prodge02  8746  ltmul12a  8751  mulgt1  8754  nndivtr  8895  addltmul  9089  elnnnn0b  9154  xnn0nnn0pnf  9186  elnnz  9197  zmulcl  9240  nn0n0n1ge2  9257  nn0lt2  9268  nn0le2is012  9269  uzind2  9299  nn0ind-raph  9304  eluzp1m1  9485  uz3m2nn  9507  supinfneg  9529  infsupneg  9530  infregelbex  9532  negm  9549  lbzbi  9550  qaddcl  9569  qmulcl  9571  qreccl  9576  elpq  9582  ledivge1le  9658  nn0ledivnn  9699  xrltne  9745  xrre  9752  xrre2  9753  xrre3  9754  ge0gtmnf  9755  xltnegi  9767  xnn0xadd0  9799  xnegdi  9800  xposdif  9814  xlesubadd  9815  iccsupr  9898  icoshft  9922  icoshftf1o  9923  fznlem  9972  fzen  9974  uzsubsubfz  9978  fzsuc2  10010  elfz1b  10021  elfz0ubfz0  10056  elfz0fzfz0  10057  fz0fzelfz0  10058  fz0fzdiffz0  10061  elfzmlbp  10063  difelfznle  10066  fzofzim  10119  eluzgtdifelfzo  10128  elfzodifsumelfzo  10132  elfzonlteqm1  10141  elfzom1p1elfzo  10145  ssfzo12bi  10156  subfzo0  10173  exbtwnzlemstep  10179  modqmuladdnn0  10299  modfzo0difsn  10326  addmodlteq  10329  frec2uzlt2d  10335  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  m1expcl2  10473  expge1  10488  leexp2r  10505  expubnd  10508  zesq  10569  expnlbnd  10575  nn0ltexp2  10619  nn0opthd  10631  faclbnd  10650  bcpasc  10675  hashprg  10717  seq3coll  10751  rexanuz  10926  rexuz3  10928  r19.29uz  10930  r19.2uz  10931  absnid  11011  leabs  11012  ltabs  11025  icodiamlt  11118  maxleast  11151  negfi  11165  climcn2  11246  climcau  11284  climcaucn  11288  sumdc  11295  fsum3cvg  11315  isumz  11326  fsumf1o  11327  fisumss  11329  isumss2  11330  fsumzcl2  11342  fsumsplit  11344  fsumsplitsnun  11356  sumsplitdc  11369  fsum2dlemstep  11371  telfsumo  11403  fsumparts  11407  fsumiun  11414  isumrpcl  11431  fproddccvg  11509  prod1dc  11523  prodssdc  11526  fprodssdc  11527  prodsnf  11529  fprodsplitdc  11533  fprod2dlemstep  11559  fprodmodd  11578  efexp  11619  efieq1re  11708  p1modz1  11730  dvds0lem  11737  dvds2ln  11760  dvdssub2  11771  dvdsadd2b  11776  dvdsabseq  11781  divconjdvds  11783  dvdsdivcl  11784  odd2np1  11806  oddge22np1  11814  opoe  11828  omoe  11829  opeo  11830  omeo  11831  m1expo  11833  nn0ehalf  11836  nn0o1gt2  11838  nno  11839  divalgb  11858  ndvdsadd  11864  zsupcllemex  11875  zssinfcl  11877  gcd0id  11908  gcdneg  11911  gcdaddm  11913  bezoutlemstep  11926  dfgcd2  11943  gcddiv  11948  dvdsmulgcd  11954  bezoutr  11961  bezoutr1  11962  uzwodc  11966  algfx  11980  lcmgcdlem  12005  lcmgcdeq  12011  coprmdvds  12020  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  isprm3  12046  dvdsnprmd  12053  prmgt1  12060  oddprmgt2  12062  isprm6  12075  cncongrprm  12085  phibndlem  12144  phimullem  12153  powm2modprm  12180  modprm0  12182  modprmn0modprm0  12184  prm23lt5  12191  pcneg  12252  pcprmpw2  12260  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  pcaddlem  12266  fldivp1  12274  pcfac  12276  oddprmdvds  12280  prmunb  12288  ennnfone  12354  unct  12371  uniopn  12599  istopon  12611  fiinbas  12647  tg2  12660  tgcl  12664  0nnei  12753  tgrest  12769  tgcn  12808  cnpnei  12819  cncnp2m  12831  lmtopcnp  12850  tx2cn  12870  txcn  12875  cnmpt21  12891  isxmet2d  12948  metrest  13106  metcnpi3  13117  tgioo  13146  fsumcncntop  13156  elcncf1di  13166  climcncf  13171  cncfco  13178  suplociccreex  13202  cnplimcim  13236  cnlimci  13242  reeff1olem  13292  efltlemlt  13295  zabsle1  13500  lgslem3  13503  lgsmod  13527  lgsdir2lem5  13533  lgsdir2  13534  lgsne0  13539  lgsdirnn0  13548  bj-charfun  13649  bj-charfunr  13652  bj-charfunbi  13653  bj-prexg  13753  peano5set  13782  bj-peano4  13797  bj-nn0suc  13806  bj-nn0sucALT  13820  bj-findis  13821  exmidsbthrlem  13861  trilpolemres  13881  trirec0  13883  nconstwlpolem  13903  neapmkv  13906