Theorem impcom 408

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 407	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpan9  507  bianir  1057  19.29r  1877  19.41v  1953  19.41  2228  nfsb4t  2497  mo4  2559  2euexv  2626  2euex  2636  raleqbidvv  3303  gencl  3486  2gencl  3487  vtocl2ga  3536  vtocl4g  3541  rspccva  3581  2reurex  3721  2reu1  3856  rexdifi  4110  sseq0  4364  r19.2z  4457  ralf0  4476  falseral0  4482  elelpwi  4575  preqsnd  4821  prproe  4868  ssuni  4898  disji2  5092  invdisjrab  5096  disjiun  5097  disjxiun  5107  trintss  5246  ssexg  5285  reusv2lem3  5360  propeqop  5469  otiunsndisj  5482  rexopabb  5490  pofun  5568  solin  5575  2optocl  5732  3optocl  5733  ssrelrn  5855  elrnmpt1  5918  resieq  5953  reuop  6250  funimaexgOLD  6593  fnun  6619  fss  6690  fun  6709  fvelimab  6919  fvmptss  6965  fvn0ssdmfun  7030  fvcofneq  7048  fmptco  7080  funsndifnop  7102  fnressn  7109  fressnfv  7111  fvn0fvelrnOLD  7114  fmptsng  7119  fvtp2g  7153  fvtp3g  7154  tpres  7155  fnex  7172  funfvima3  7191  isores3  7285  tfisg  7795  dmfex  7849  opreuopreu  7971  releldmdifi  7982  funeldmdif  7985  el2mpocsbcl  8022  f1o2ndf1  8059  frxp  8063  fnse  8070  frxp2  8081  frxp3  8088  poseq  8095  ressuppssdif  8121  funsssuppss  8126  suppssOLD  8131  mpoxopxnop0  8151  reldmtpos  8170  frrlem8  8229  fpr2a  8238  wfrfunOLD  8270  wfrlem12OLD  8271  smores  8303  tfrlem7  8334  tz7.48-2  8393  tz7.49  8396  oacl  8486  omcl  8487  oecl  8488  oarec  8514  oewordri  8544  oeworde  8545  oelim2  8547  oeoa  8549  oeoelem  8550  oeoe  8551  nnacl  8563  nnmcl  8564  nnecl  8565  nnmsucr  8577  2ecoptocl  8754  fsetprcnex  8807  undifixp  8879  ssctOLD  9003  xpf1o  9090  limensuc  9105  unfi  9123  imafi  9126  en1eqsn  9225  ac6sfi  9238  frfi  9239  difinf  9267  f1dmvrnfibi  9287  f1vrnfibi  9288  suppeqfsuppbi  9328  elfiun  9375  dffi3  9376  infsupprpr  9449  xpwdomg  9530  infdiffi  9603  ttrclselem2  9671  epfrs  9676  frmin  9694  frr2  9705  rankxpsuc  9827  updjud  9879  tskwe  9895  infxpenlem  9958  fseqenlem1  9969  kmlem2  10096  nnadju  10142  cff1  10203  cflim2  10208  sornom  10222  infpssrlem4  10251  fin23lem26  10270  fin23lem30  10287  fin23lem34  10291  isf32lem11  10308  fin67  10340  isfin7-2  10341  fin1a2lem10  10354  axcc2lem  10381  axdc2lem  10393  axdc3lem2  10396  axdc3lem4  10398  axdc4lem  10400  iunfo  10484  tsk0  10708  gruina  10763  grur1a  10764  mulcanenq  10905  reclem2pr  10993  supsrlem  11056  supsr  11057  ax1rid  11106  negf1o  11594  mulgt1  12023  lbreu  12114  nnindd  12182  nnaddcl  12185  nnmulcl  12186  nn0n0n1ge2b  12490  nn0indd  12609  fzind  12610  fnn0ind  12611  uzaddcl  12838  uzinfi  12862  nn01to3  12875  elpq  12909  xmulasslem2  13211  supxrunb1  13248  supxrunb2  13249  infmremnf  13272  infmrp1  13273  uzsubsubfz  13473  elfz0ubfz0  13555  fz0fzdiffz0  13560  elfzmlbp  13562  fzofzim  13629  elfzom1elp1fzo  13649  ssfzo12bi  13677  fzonfzoufzol  13685  elfznelfzob  13688  injresinjlem  13702  injresinj  13703  modaddmodup  13849  modfzo0difsn  13858  modsumfzodifsn  13859  addmodlteq  13861  om2uzlti  13865  fsequb  13890  ssnn0fi  13900  ser1const  13974  expcllem  13988  expeq0  14008  expmordi  14082  expnngt1  14154  faclbnd  14200  hashf1rn  14262  hashgadd  14287  hashunx  14296  hashnn0n0nn  14301  hashgt0elex  14311  hashss  14319  hashfzp1  14341  hashxp  14344  hashmap  14345  hashimarni  14351  seqcoll  14375  hash2exprb  14382  hashge2el2difr  14392  elss2prb  14398  hashdifsnp1  14407  fi1uzind  14408  brfi1indALT  14411  lswlgt0cl  14469  swrdnd  14554  swrdnnn0nd  14556  swrdnd0  14557  swrd0  14558  swrdsbslen  14564  swrdspsleq  14565  pfxsuff1eqwrdeq  14599  swrdswrdlem  14604  swrdswrd  14605  wrd2ind  14623  pfxccatin12lem2a  14627  swrdccatin2  14629  pfxccatin12lem2  14631  pfxccatin12lem3  14632  pfxccatin12  14633  pfxccat3  14634  swrdccat  14635  pfxccat3a  14638  swrdccat3blem  14639  repswswrd  14684  repswrevw  14687  cshwmodn  14695  cshwsublen  14696  cshwidxmod  14703  cshwidxmodr  14704  cshf1  14710  2cshw  14713  cshweqrep  14721  cshw1  14722  2cshwcshw  14726  cshwcshid  14728  cshwcsh2id  14729  wrdlen2i  14843  2swrd2eqwrdeq  14854  wwlktovfo  14859  relexpsucnnl  14927  rtrclreclem3  14957  rtrclreclem4  14958  relexpindlem  14960  r19.29uz  15247  caubnd  15255  sqreu  15257  climshft  15470  climub  15558  climserle  15559  sumss  15620  sumss2  15622  modfsummods  15689  o1fsum  15709  binom  15726  climcndslem1  15745  climcndslem2  15746  cvgrat  15779  clim2prod  15784  prodfn0  15790  prodfrec  15791  ntrivcvgfvn0  15795  fprodn0  15873  fprodmodd  15891  fprodefsum  15988  demoivreALT  16094  ruclem8  16130  dvdsaddre2b  16200  dvdsdivcl  16209  dvdsfac  16219  oddnn02np1  16241  oddge22np1  16242  evennn02n  16243  evennn2n  16244  m1exp1  16269  nn0o  16276  pwp1fsum  16284  flodddiv4  16306  smu01lem  16376  dvdslegcd  16395  gcdneg  16413  dfgcd2  16438  seq1st  16458  alginv  16462  lcmf  16520  lcmftp  16523  lcmfunsnlem2lem2  16526  lcmfunsnlem  16528  lcmfun  16532  ncoprmgcdne1b  16537  coprmproddvdslem  16549  coprmproddvds  16550  cncongr1  16554  prmdvdsexp  16602  prmndvdsfaclt  16612  ncoprmlnprm  16614  fvprmselgcd1  16928  prmgaplem6  16939  prmgaplem7  16940  prmgaplem8  16941  cshwshashlem1  16979  setsstruct2  17057  setsstruct  17059  inveq  17671  catsubcat  17739  initoeu2lem0  17913  initoeu2lem1  17914  funcestrcsetclem8  18049  funcestrcsetclem9  18050  fthestrcsetc  18052  fullestrcsetc  18053  funcsetcestrclem9  18065  fthsetcestrc  18067  fullsetcestrc  18068  lubss  18416  lubel  18417  issstrmgm  18522  mgmb1mgm1  18524  sgrpidmnd  18575  frmdgsum  18686  smndex1mndlem  18733  mgm2nsgrplem3  18744  dfgrp2  18789  cyccom  19010  gaass  19091  gsumwrev  19161  symgextf1lem  19216  symgextf1  19217  fvcosymgeq  19225  gsmsymgreq  19228  symgfixelsi  19231  pmtrprfv3  19250  symggen  19266  pmtrprfval  19283  gsumzres  19700  gsumpr  19746  gsumzunsnd  19747  srgmulgass  19962  srgbinom  19976  0ringnnzr  20212  lmodvsmmulgdi  20414  lmodfopnelem1  20415  rmodislmodlem  20446  cnfldmulg  20866  cnfldexp  20867  psgndiflemB  21041  assamulgscm  21341  gsumply1subr  21642  gsummoncoe1  21712  pf1ind  21758  matmulcell  21831  mat1dimscm  21861  dmatmul  21883  dmatscmcl  21889  scmataddcl  21902  scmatsubcl  21903  scmatsgrp1  21908  mavmulsolcl  21937  ma1repveval  21957  1marepvmarrepid  21961  symgmatr01lem  22039  slesolvec  22065  cramerimplem2  22070  decpmatmullem  22157  pm2mpf1  22185  mp2pm2mplem4  22195  monmat2matmon  22210  chpscmat  22228  chpscmatgsumbin  22230  fvmptnn04ifb  22237  chfacfscmul0  22244  chfacfscmulgsum  22246  chfacfpmmul0  22248  chfacfpmmulgsum  22250  cpmadugsumlemF  22262  toprntopon  22311  clsss  22442  ntrss  22443  restntr  22570  cmpsublem  22787  cmpsub  22788  2ndcrest  22842  txindislem  23021  t0kq  23206  filufint  23308  fbflim2  23365  flftg  23384  alexsubALTlem4  23438  cnextfvval  23453  ustuqtop4  23633  xmettri2  23730  mettri  23742  metss  23901  tngngp3  24057  clmvscom  24490  lmmbr  24659  caublcls  24710  lmcau  24714  ovolunlem1a  24897  nulmbl2  24937  voliunlem1  24951  iunmbl  24954  volsup  24957  dvlip  25394  dvfsumle  25422  degltlem1  25474  ply1divex  25538  plyco  25639  dgrnznn  25645  dvnply2  25684  plydivex  25694  aannenlem2  25726  aaliou3lem2  25740  ulmcau  25791  zabsle1  26681  gausslemma2dlem1a  26750  gausslemma2dlem2  26752  gausslemma2dlem3  26753  gausslemma2dlem4  26754  2lgslem1a1  26774  2sqnn0  26823  2sqreulem1  26831  2sqreunnlem1  26834  dchrisumlem1  26874  dchrisumlem2  26875  dchrisumlem3  26876  qabvle  27010  ostthlem2  27013  ostth2lem2  27019  nosupbnd1lem5  27097  noinfbnd1lem5  27112  nocvxminlem  27160  nocvxmin  27161  slerec  27201  madebdaylemold  27270  tgjustr  27479  axeuclidlem  27974  incistruhgr  28093  umgredgprv  28121  umgrpredgv  28154  usgredgprvALT  28206  uhgr2edg  28219  usgredg2vlem2  28237  lfuhgr1v0e  28265  subgrfun  28292  umgrres1lem  28321  upgrres1  28324  fusgrfis  28341  uhgrnbgr0nb  28365  nbgr1vtx  28369  nb3grprlem1  28391  uvtx01vtx  28408  fusgrn0degnn0  28510  vtxdginducedm1lem4  28553  finsumvtxdg2size  28561  wlkl1loop  28649  wlkres  28681  lfgrwlknloop  28700  pthdadjvtx  28741  upgr2pthnlp  28743  upgrwlkdvdelem  28747  upgrwlkdvde  28748  uhgrwkspthlem2  28765  usgr2trlspth  28772  usgr2pth  28775  pthdlem2lem  28778  lfgrn1cycl  28813  uspgrn2crct  28816  crctcshwlkn0lem3  28820  crctcshwlkn0lem4  28821  crctcshwlkn0lem5  28822  iswspthsnon  28864  wlkiswwlks1  28875  wlklnwwlkln1  28876  wlkiswwlks2  28883  wlkiswwlksupgr2  28885  wlklnwwlkln2lem  28890  wlknwwlksnbij  28896  wwlksnred  28900  wwlksnext  28901  wwlksnredwwlkn  28903  wwlksnredwwlkn0  28904  wwlksnextfun  28906  wwlksnextinj  28907  wwlksnextsurj  28908  wspthsnonn0vne  28925  wspn0  28932  wwlks2onv  28961  elwwlks2  28974  elwspths2spth  28975  rusgrnumwwlk  28983  clwwlkccatlem  28996  clwlkclwwlklem2a1  28999  clwlkclwwlklem2fv2  29003  clwlkclwwlklem2a4  29004  clwlkclwwlklem2a  29005  clwlkclwwlklem2  29007  clwlkclwwlkf1lem3  29013  clwwisshclwwslem  29021  clwwisshclwwsn  29023  erclwwlktr  29029  isclwwlknx  29043  clwwlkinwwlk  29047  clwwlkel  29053  clwwlkf  29054  clwwlkf1  29056  clwwlkfo  29057  clwwlkext2edg  29063  wwlksext2clwwlk  29064  wwlksubclwwlk  29065  clwwlknscsh  29069  erclwwlkntr  29078  eleclclwwlkn  29083  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  clwwlknon0  29100  clwwlknonel  29102  clwwlknon1  29104  clwwlknonwwlknonb  29113  clwwlknonex2lem2  29115  clwwlknun  29119  clwwlkvbij  29120  upgr3v3e3cycl  29187  uhgr3cyclex  29189  upgr4cycl4dv4e  29192  eulerpath  29248  eucrctshift  29250  eucrct2eupth  29252  1to2vfriswmgr  29286  1to3vfriswmgr  29287  3cyclfrgrrn1  29292  4cycl2vnunb  29297  frgrwopreglem2  29320  frgrwopreglem3  29321  frgrwopreglem5ALT  29329  fusgr2wsp2nb  29341  2clwwlk2clwwlklem  29353  2clwwlk2clwwlk  29357  numclwwlk1lem2f1  29364  numclwwlk1lem2fo  29365  numclwwlk1  29368  clwwlknonclwlknonf1o  29369  dlwwlknondlwlknonf1o  29372  numclwlk1  29378  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  numclwwlk5  29395  frgrreg  29401  frgrregord013  29402  friendship  29406  nsnlplig  29486  nsnlpligALT  29487  isgrpo  29502  vcdi  29570  vcdir  29571  vcass  29572  nmosetre  29769  hlim2  30197  shscli  30322  chintcli  30336  dfch2  30412  spansncvi  30657  nmopsetretALT  30868  nmfnsetre  30882  lnopl  30919  lnfnl  30936  pjss2coi  31169  pjorthcoi  31174  pjscji  31175  pjssdif2i  31179  pjclem4a  31203  pj3lem1  31211  strlem5  31260  hstrlem5  31268  cvmdi  31329  mdslmd3i  31337  atcv1  31385  atcvat4i  31402  cdj3lem2a  31441  cdj3lem3a  31444  opreu2reuALT  31469  iuninc  31546  disji2f  31562  disjif2  31566  fmptcof2  31640  xrsmulgzz  31939  ofldchr  32180  esumfzf  32757  issgon  32811  voliune  32917  volfiniune  32918  rrvsum  33143  bnj228  33436  bnj1294  33518  bnj229  33585  bnj607  33617  bnj908  33632  bnj953  33640  bnj1118  33685  bnj1174  33704  bnj1388  33734  funen1cnv  33781  acycgrsubgr  33839  cvmliftlem15  33979  satfsschain  34045  satfdm  34050  satf0op  34058  fmla0xp  34064  gonarlem  34075  goalrlem  34077  satffunlem1lem1  34083  satffunlem2lem1  34085  dmopab3rexdif  34086  satefvfmla0  34099  prv1n  34112  iprodefisumlem  34399  faclimlem1  34402  dfon2lem6  34449  idinside  34745  onsucconni  34985  axc11n11r  35224  bj-brrelex12ALT  35611  bj-snmoore  35657  bj-finsumval0  35829  exlimim  35886  exellim  35888  icoreclin  35901  difunieq  35918  fvineqsneq  35956  pibt2  35961  wl-spae  36053  wl-aleq  36067  fin2so  36138  matunitlindf  36149  poimirlem4  36155  poimirlem26  36177  itg2addnclem  36202  upixp  36261  welb  36268  sdclem2  36274  metf1o  36287  sstotbnd3  36308  isbndx  36314  ismtycnv  36334  heiborlem4  36346  bfplem1  36354  opidonOLD  36384  grpomndo  36407  ax12eq  37476  ax12el  37477  cvrat4  37979  nn0addcom  40977  nn0mulcom  40981  mzpexpmpt  41126  diophren  41194  rmxypos  41329  jm2.17a  41342  jm2.17b  41343  rmygeid  41346  jm2.18  41370  jm2.25  41381  jm2.15nn0  41385  jm2.16nn0  41386  pwslnm  41479  isnumbasgrplem1  41486  dgraalem  41530  onuniintrab  41618  onsupuni  41621  onsupcl3  41625  naddonnn  41789  naddwordnexlem2  41792  relexpiidm  42098  relexpmulnn  42103  relexpmulg  42104  relexp01min  42107  relexp0a  42110  relexpxpmin  42111  clsk1indlem3  42437  grucollcld  42662  dvgrat  42714  radcnvrat  42716  sspwimpcf  43324  sspwimpcfVD  43325  e2ebindALT  43333  et-sqrtnegnre  45234  fsetprcnexALT  45416  eu2ndop1stv  45477  afvfv0bi  45504  afveu  45505  afvres  45524  aovmpt4g  45553  ndmaovass  45558  ndmaovdistr  45559  afv2orxorb  45580  afv2eu  45590  imarnf1pr  45634  nltle2tri  45665  fzopredsuc  45675  subsubelfzo0  45678  fzoopth  45679  2ffzoeq  45680  smonoord  45683  elsetpreimafvssdm  45698  iccpartres  45730  iccpartiltu  45734  iccpartigtl  45735  iccpartgt  45739  icceuelpartlem  45747  fargshiftf1  45753  ichnreuop  45784  ichreuopeq  45785  elsprel  45787  sprsymrelfo  45809  prproropf1olem4  45818  paireqne  45823  sbcpr  45833  reupr  45834  goldbachth  45859  fmtnoprmfac1  45877  fmtnoprmfac2  45879  prmdvdsfmtnof1lem2  45897  lighneallem2  45918  lighneallem4  45922  requad2  45935  even3prm2  46031  fpprwpprb  46052  gbegt5  46073  sbgoldbwt  46089  sbgoldbm  46096  nnsum3primesgbe  46104  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbndlem4  46120  bgoldbtbnd  46121  isomuspgrlem1  46139  isomuspgrlem2d  46143  upgrwlkupwlk  46162  uspgropssxp  46166  uspgrsprfo  46170  mgmpropd  46189  isassintop  46264  lidldomn1  46339  lidlmmgm  46343  2zlidl  46352  2zrngamgm  46357  2zrngmmgm  46364  rnghmsscmap  46392  rnghmsubcsetclem2  46394  rngcinv  46399  rngccatidALTV  46407  rngcinvALTV  46411  funcrngcsetc  46416  funcrngcsetcALT  46417  rhmsscmap  46438  rhmsubcsetclem2  46440  rhmsubcrngclem2  46446  funcringcsetc  46453  funcringcsetcALTV2lem9  46462  ringccatidALTV  46470  srhmsubc  46494  rhmsubclem4  46507  srhmsubcALTV  46512  rhmsubcALTVlem4  46525  lmodvsmdi  46578  ply1mulgsumlem1  46587  ply1mulgsumlem2  46588  lincdifsn  46625  lincsumcl  46632  lincscmcl  46633  lincext3  46657  lindslinindsimp1  46658  lindslinindsimp2lem5  46663  snlindsntor  46672  lincresunit2  46679  lincresunit3lem2  46681  zgtp1leeq  46722  m1modmmod  46727  elbigo2  46758  fllog2  46774  digexp  46813  dig1  46814  nn0sumshdiglemA  46825  nn0sumshdiglemB  46826  1arymaptf1  46848  2arymaptf1  46859  rrxlinec  46942  eenglngeehlnm  46945  rrx2linest  46948  itsclc0yqsol  46970  itsclc0xyqsol  46974