Theorem impcom 445

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
impcom	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 32	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 444	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385

This theorem is referenced by:  mpan9  485  bianir  1001  19.29r  1790  19.41v  1901  equtr2OLD  1943  equvinvOLD  1949  19.41  2090  nfsb4t  2377  2euex  2532  gencl  3208  2gencl  3209  vtocl4g  3250  rspccva  3281  sseq0  3927  minelOLD  3986  r19.2z  4012  elelpwi  4119  eqoreldifOLD  4173  ssuni  4395  ssuniOLD  4396  disji2  4569  invdisjrab  4572  disjiun  4573  disjxiun  4579  trint0  4698  ssexg  4732  reusv2lem3  4797  propeqop  4895  otiunsndisj  4905  pofun  4975  solin  4982  2optocl  5119  3optocl  5120  ssrelrn  5237  elrnmpt1  5295  resieq  5327  funimaexg  5889  fnun  5911  fss  5969  fun  5979  fvelimab  6163  fvmptss  6201  fvn0ssdmfun  6258  fvcofneq  6275  fmptco  6303  funsndifnop  6321  fnressn  6330  fressnfv  6332  fvn0fvelrn  6335  fmptsng  6339  fvtp2g  6369  fvtp3g  6370  tpres  6371  fnex  6386  funfvima3  6399  isores3  6485  dmfex  7017  el2mpt2csbcl  7137  f1o2ndf1  7172  frxp  7174  fnse  7181  ressuppssdif  7203  funsssuppss  7208  suppss  7212  mpt2xopxnop0  7228  reldmtpos  7247  wfrfun  7312  wfrlem12  7313  smores  7336  tfrlem7  7366  tz7.48-2  7424  tz7.49  7427  oacl  7502  omcl  7503  oecl  7504  oarec  7529  oewordri  7559  oeworde  7560  oelim2  7562  oeoa  7564  oeoelem  7565  oeoe  7566  nnacl  7578  nnmcl  7579  nnecl  7580  nnmsucr  7592  2ecoptocl  7725  undifixp  7830  ssct  7926  xpf1o  8007  limensuc  8022  ac6sfi  8089  frfi  8090  difinf  8115  f1dmvrnfibi  8133  f1vrnfibi  8134  suppeqfsuppbi  8172  elfiun  8219  dffi3  8220  xpwdomg  8373  preleq  8397  infdiffi  8438  epfrs  8490  rankxpsuc  8628  tskwe  8659  infxpenlem  8719  fseqenlem1  8730  kmlem2  8856  cff1  8963  cflim2  8968  sornom  8982  infpssrlem4  9011  fin23lem26  9030  fin23lem30  9047  fin23lem34  9051  isf32lem11  9068  fin67  9100  isfin7-2  9101  fin1a2lem10  9114  axcc2lem  9141  axdc2lem  9153  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  iunfo  9240  tsk0  9464  gruina  9519  grur1a  9520  mulcanenq  9661  reclem2pr  9749  supsrlem  9811  supsr  9812  ax1rid  9861  negf1o  10339  mulgt1  10761  fiminre  10851  lbreu  10852  nnaddcl  10919  nnmulcl  10920  nn0n0n1ge2b  11236  nn0indd  11350  fzind  11351  fnn0ind  11352  uzaddcl  11620  uzinfi  11644  nn01to3  11657  xmulasslem2  11984  supxrunb1  12021  supxrunb2  12022  infmremnf  12044  infmrp1  12045  uzsubsubfz  12234  elfz1b  12279  elfz0ubfz0  12312  fz0fzdiffz0  12317  elfzmlbp  12319  fzofzim  12382  elfzom1elp1fzo  12402  elfzom1p1elfzo  12414  ssfzo12bi  12429  fzonfzoufzol  12437  elfznelfzob  12440  injresinjlem  12450  injresinj  12451  modaddmodup  12595  modfzo0difsn  12604  modsumfzodifsn  12605  addmodlteq  12607  om2uzlti  12611  fsequb  12636  ssnn0fi  12646  ser1const  12719  expcllem  12733  expeq0  12752  faclbnd  12939  faclbnd6  12948  hasheqf1oiOLD  13003  hashf1rn  13004  hashf1rnOLD  13005  hashgadd  13027  hashunx  13036  hashnn0n0nn  13041  hashgt0elex  13050  hashss  13058  hashfzp1  13078  hashxp  13081  hashimarni  13086  seqcoll  13105  hash2exprb  13110  hashge2el2difr  13118  elss2prb  13123  brfi1indlem  13133  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  lswlgt0cl  13209  swrdnd  13284  swrd0  13286  swrdsbslen  13300  swrdspsleq  13301  2swrd1eqwrdeq  13306  swrdswrdlem  13311  swrdswrd  13312  wrd2ind  13329  swrdccatfn  13333  swrdccatin1  13334  swrdccatin12lem2a  13336  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccatin12  13342  swrdccat3  13343  swrdccat  13344  swrdccat3blem  13346  repswswrd  13382  repswrevw  13384  cshwmodn  13392  cshwsublen  13393  cshwidxmod  13400  cshwidxmodr  13401  cshf1  13407  2cshw  13410  cshweqrep  13418  cshw1  13419  2cshwcshw  13422  cshwcshid  13424  cshwcsh2id  13425  wrdlen2i  13534  2swrd2eqwrdeq  13544  wwlktovfo  13549  relexpsucnnl  13620  rtrclreclem3  13648  rtrclreclem4  13649  relexpindlem  13651  cjexp  13738  absexp  13892  r19.29uz  13938  caubnd  13946  sqreu  13948  climshft  14155  climub  14240  climserle  14241  sumss  14302  sumss2  14304  modfsummods  14366  o1fsum  14386  binom  14401  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  pwm1geoser  14439  cvgrat  14454  clim2prod  14459  prodfn0  14465  prodfrec  14466  ntrivcvgfvn0  14470  fprodn0  14548  fprodmodd  14567  fprodefsum  14664  demoivreALT  14770  znnenlem  14779  ruclem8  14805  dvdsaddre2b  14867  dvdsdivcl  14876  dvdsfac  14886  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  m1exp1  14931  nn0o  14937  sumeven  14948  pwp1fsum  14952  flodddiv4  14975  smu01lem  15045  dvdslegcd  15064  gcdneg  15081  dfgcd2  15101  gcdmultiple  15107  seq1st  15122  alginv  15126  lcmf  15184  lcmftp  15187  lcmfunsnlem2lem2  15190  lcmfunsnlem  15192  lcmfun  15196  ncoprmgcdne1b  15201  coprmproddvdslem  15214  coprmproddvds  15215  cncongr1  15219  prmdvdsexp  15265  prmndvdsfaclt  15273  ncoprmlnprm  15274  fvprmselgcd1  15587  prmgaplem6  15598  prmgaplem7  15599  prmgaplem8  15600  cshwshashlem1  15640  inveq  16257  catsubcat  16322  initoeu2lem0  16486  initoeu2lem1  16487  funcestrcsetclem8  16610  funcestrcsetclem9  16611  fthestrcsetc  16613  fullestrcsetc  16614  funcsetcestrclem9  16626  fthsetcestrc  16628  fullsetcestrc  16629  lubss  16944  lubel  16945  issstrmgm  17075  mgmb1mgm1  17077  frmdgsum  17222  mgm2nsgrplem3  17230  dfgrp2  17270  gaass  17553  gsumwrev  17619  symgextf1lem  17663  symgextf1  17664  fvcosymgeq  17672  gsmsymgreq  17675  symgfixelsi  17678  pmtrprfv3  17697  symggen  17713  pmtrprfval  17730  gsumzres  18133  gsumzunsnd  18178  srgmulgass  18354  srgbinom  18368  lmodvsmmulgdi  18721  lmodfopnelem1  18722  0ringnnzr  19090  assamulgscm  19171  gsumply1subr  19425  gsummoncoe1  19495  pf1ind  19540  cnfldmulg  19597  cnfldexp  19598  psgndiflemB  19765  matmulcell  20070  mat1dimscm  20100  dmatmul  20122  dmatscmcl  20128  scmataddcl  20141  scmatsubcl  20142  scmatsgrp1  20147  mavmulsolcl  20176  ma1repveval  20196  1marepvmarrepid  20200  symgmatr01lem  20278  slesolvec  20304  cramerimplem2  20309  decpmatmullem  20395  pm2mpf1  20423  mp2pm2mplem4  20433  monmat2matmon  20448  chpscmat  20466  chpscmatgsumbin  20468  fvmptnn04ifb  20475  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  cpmadugsumlemF  20500  clsss  20668  ntrss  20669  restntr  20796  cmpsublem  21012  cmpsub  21013  2ndcrest  21067  txindislem  21246  t0kq  21431  filufint  21534  fbflim2  21591  flftg  21610  alexsubALTlem4  21664  cnextfvval  21679  tmdmulg  21706  ustuqtop4  21858  xmettri2  21955  mettri  21967  metss  22123  tngngp3  22270  clmvscom  22698  lmmbr  22864  caublcls  22915  lmcau  22919  ovolunlem1a  23071  nulmbl2  23111  voliunlem1  23125  iunmbl  23128  volsup  23131  dvlip  23560  dvfsumle  23588  degltlem1  23636  ply1divex  23700  plyco  23801  dgrnznn  23807  dvnply2  23846  plydivex  23856  aannenlem2  23888  aaliou3lem2  23902  ulmcau  23953  zabsle1  24821  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem4  24894  2lgslem1a1  24914  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  qabvle  25114  ostthlem2  25117  ostth2lem2  25123  axeuclidlem  25642  incistruhgr  25746  umgredgprv  25773  umgrpredgav  25813  usgra2edg  25911  usgraedg4  25916  usgraidx2vlem2  25921  nbusgra  25957  nbgraf1olem5  25974  nb3graprlem1  25980  nb3graprlem2  25981  cusgrarn  25988  nbcusgra  25992  cusgrasize2inds  26005  sizeusglecusglem1  26012  uvtxnbgra  26021  iswlkg  26052  wlkn0  26055  usgrwlknloop  26093  redwlk  26136  wlkdvspthlem  26137  usgra2adedgwlkonALT  26144  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  usgra2wlkspth  26149  fargshiftf1  26165  usgrcyclnl1  26168  usgrcyclnl2  26169  nvnencycllem  26171  constr3trllem2  26179  wwlknimp  26215  wlkiswwlk1  26218  wlkiswwlk2  26225  wlklniswwlkn1  26227  wlklniswwlkn2  26228  vfwlkniswwlkn  26234  wwlknext  26252  wwlknredwwlkn  26254  wwlknredwwlkn0  26255  wwlkextfun  26257  wwlkextinj  26258  wwlkextsur  26259  wwlkextproplem3  26271  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkel  26321  clwwlkf1  26324  clwwlkfo  26325  clwwlknwwlkncl  26328  clwwlkext2edg  26330  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwwisshclwwlem  26334  clwwisshclww  26335  clwwisshclwwn  26336  erclwwlktr  26343  clwwlknscsh  26347  erclwwlkntr  26355  eleclclwwlkn  26360  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlkfclwwlk  26371  clwlkfoclwwlk  26372  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  usg2spthonot0  26416  rusgrasn  26472  rusgranumwlk  26484  clwlknclwlkdifs  26487  frgra1v  26525  1to2vfriswmgra  26533  1to3vfriswmgra  26534  3cyclfrgrarn1  26539  4cycl2vnunb  26544  frgrancvvdeqlem3  26559  frgrawopreglem3  26573  frgrawopreglem4  26574  frgrawopreg  26576  frg2woteqm  26586  2spotdisj  26588  2spotiundisj  26589  usg2spot2nb  26592  extwwlkfablem1  26601  clwwlkextfrlem1  26603  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwwlkovgelim  26616  numclwlk1lem2foa  26618  numclwlk1lem2f1  26621  numclwlk1lem2fo  26622  numclwwlk1  26625  numclwlk2lem2f  26630  numclwlk2lem2f1o  26632  numclwwlk5  26639  frgrareg  26644  frgraregord013  26645  friendship  26649  isgrpo  26735  vcdi  26804  vcdir  26805  vcass  26806  nmosetre  27003  hlim2  27433  shscli  27560  chintcli  27574  dfch2  27650  spansncvi  27895  nmopsetretALT  28106  nmfnsetre  28120  lnopl  28157  lnfnl  28174  pjss2coi  28407  pjorthcoi  28412  pjscji  28413  pjssdif2i  28417  pjclem4a  28441  pj3lem1  28449  strlem5  28498  hstrlem5  28506  cvmdi  28567  mdslmd3i  28575  atcv1  28623  atcvat4i  28640  cdj3lem2a  28679  cdj3lem3a  28682  iuninc  28761  disji2f  28772  disjif2  28776  fmptcof2  28839  nnindd  28953  xrsmulgzz  29009  ofldchr  29145  esumfzf  29458  issgon  29513  voliune  29619  volfiniune  29620  rrvsum  29843  bnj228  30057  bnj1294  30142  bnj229  30208  bnj607  30240  bnj908  30255  bnj953  30263  bnj1118  30306  bnj1174  30325  bnj1388  30355  cvmliftlem15  30534  iprodefisumlem  30879  faclimlem1  30882  dfon2lem6  30937  tfisg  30960  poseq  30994  frrlem4  31027  frrlem5c  31030  frrlem11  31036  nodenselem5  31084  nocvxminlem  31089  nocvxmin  31090  idinside  31361  nn0prpw  31488  onsucconi  31606  axc11n11r  31860  bj-finsumval0  32324  exlimim  32365  exellim  32368  icoreclin  32381  wl-spae  32485  wl-aleq  32501  fin2so  32566  matunitlindf  32577  poimirlem4  32583  poimirlem26  32605  itg2addnclem  32631  upixp  32694  welb  32701  sdclem2  32708  metf1o  32721  sstotbnd3  32745  isbndx  32751  ismtycnv  32771  heiborlem4  32783  bfplem1  32791  opidonOLD  32821  grpomndo  32844  ax12eq  33244  ax12el  33245  cvrat4  33747  mzpexpmpt  36326  diophren  36395  expmordi  36530  rmxypos  36532  jm2.17a  36545  jm2.17b  36546  rmygeid  36549  jm2.18  36573  jm2.25  36584  jm2.15nn0  36588  jm2.16nn0  36589  pwslnm  36682  isnumbasgrplem1  36690  dgraalem  36734  relexpiidm  37015  relexpmulnn  37020  relexpmulg  37021  relexp01min  37024  relexp0a  37027  relexpxpmin  37028  clsk1indlem3  37361  dvgrat  37533  radcnvrat  37535  sspwimpcf  38178  sspwimpcfVD  38179  e2ebindALT  38187  2reurex  39830  2reu1  39835  eu2ndop1stv  39851  afvfv0bi  39881  afveu  39882  afvres  39901  aovmpt4g  39930  ndmaovass  39935  ndmaovdistr  39936  nltle2tri  39942  smonoord  39944  fzopredsuc  39946  iccpartres  39956  iccpartiltu  39960  iccpartigtl  39961  iccpartgt  39965  icceuelpartlem  39973  goldbachth  39997  fmtnoprmfac1  40015  fmtnoprmfac2  40017  prmdvdsfmtnof1lem2  40035  lighneallem2  40061  lighneallem4  40065  gbegt5  40183  bgoldbwt  40199  nnsum3primesgbe  40208  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxsuff1eqwrdeq  40270  pfxccatin12lem2  40287  pfxccatin12  40288  pfxccat3  40289  pfxccat3a  40292  cshword2  40300  falseral0  40308  imarnf1pr  40326  subsubelfzo0  40359  fzoopth  40360  2ffzoeq  40361  usgredgprvALT  40422  uhgr2edg  40435  usgredg2vlem2  40453  lfuhgr1v0e  40480  subgrfun  40505  umgrres1lem  40529  upgrres1  40532  fusgrfis  40549  uhgrnbgr0nb  40576  nbgr1vtx  40580  nb3grprlem1  40608  uvtxa01vtx0  40623  uvtx2vtx1edg  40625  cusgrsize2inds  40669  fusgrn0degnn0  40714  upgrewlkle2  40808  1wlkl1loop  40842  upgr1wlkwlk  40847  upgrwlkedg  40850  1wlkres  40879  lfgr1wlknloop  40898  pthdadjvtx  40936  upgr2pthnlp  40938  upgrwlkdvdelem  40942  upgrwlkdvde  40943  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2trlspth  40967  usgr2pth  40970  pthdlem2lem  40973  lfgrn1cycl  41008  uspgrn2crct  41011  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  wspthnonp  41055  1wlkiswwlks1  41064  1wlklnwwlkln1  41065  1wlkiswwlks2  41072  1wlkiswwlksupgr2  41074  1wlklnwwlkln2lem  41079  wwlksnred  41098  wwlksnext  41099  wwlksnredwwlkn  41101  wwlksnredwwlkn0  41102  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextsur  41106  wspthsnonn0vne  41124  wspn0  41131  wwlks2onv  41158  2wspdisj  41165  elwwlks2  41170  elwspths2spth  41171  rusgrnumwwlk  41178  clwwlknclwwlkdifs  41181  isclwwlksnx  41197  clwlkclwwlklem2a1  41201  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlksel  41221  clwwlksf  41222  clwwlksf1  41224  clwwlksfo  41225  clwwlksnwwlkncl  41228  clwwlksvbij  41229  clwwlksext2edg  41230  wwlksext2clwwlk  41231  wwlksubclwwlks  41232  clwwisshclwwslem  41234  clwwisshclwwsn  41236  erclwwlkstr  41243  clwwlksnscsh  41247  erclwwlksntr  41255  eleclclwwlksn  41260  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlksfclwwlk  41269  clwlksfoclwwlk  41270  clwwlksnun  41281  upgr3v3e3cycl  41347  uhgr3cyclex  41349  upgr4cycl4dv4e  41352  upgreupthi  41376  eulerpath  41409  eucrctshift  41411  eucrct2eupth  41413  1to2vfriswmgr  41449  1to3vfriswmgr  41450  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  frgrncvvdeqlem3  41471  frgrwopreglem3  41483  frgrwopreglem4  41484  frgrwopreg  41486  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  av-clwwlkextfrlem1  41509  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwlk1lem2f1  41524  av-numclwlk1lem2fo  41525  av-numclwwlk1  41528  av-numclwlk2lem2f  41533  av-numclwlk2lem2f1o  41535  av-numclwwlk5  41542  av-frgrareg  41548  av-frgraregord013  41549  av-friendship  41553  mgmpropd  41565  isassintop  41636  lidldomn1  41711  lidlmmgm  41715  2zlidl  41724  2zrngamgm  41729  2zrngmmgm  41736  rnghmsscmap  41766  rnghmsubcsetclem2  41768  rngcinv  41773  rngccatidALTV  41781  rngcinvALTV  41785  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscmap  41812  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  ringcinv  41824  funcringcsetc  41827  funcringcsetcALTV2lem9  41836  ringccatidALTV  41844  ringcinvALTV  41848  srhmsubc  41868  rhmsubclem4  41881  srhmsubcALTV  41887  rhmsubcALTVlem4  41900  gsumpr  41932  lmodvsmdi  41957  ply1mulgsumlem1  41968  ply1mulgsumlem2  41969  lincdifsn  42007  lincsumcl  42014  lincscmcl  42015  lincext3  42039  lindslinindsimp1  42040  lindslinindsimp2lem5  42045  snlindsntor  42054  lincresunit2  42061  lincresunit3lem2  42063  lincresunit3  42064  zgtp1leeq  42105  m1modmmod  42110  elbigo2  42144  fllog2  42160  digexp  42199  dig1  42200  nn0sumshdiglemA  42211  nn0sumshdiglemB  42212