Theorem impcom 413

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 33	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 412	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpan9  516  anbiim  653  bianir  1074  19.29r  1909  19.41v  1984  19.41  2275  nfsb4t  2531  mo4  2594  2euexv  2659  2euex  2669  gencl  3495  2gencl  3496  vtocl2ga  3541  vtocl2gaf  3542  vtocl3gaf  3543  vtocl3ga  3544  vtocl4g  3545  vtocl4ga  3546  rspccva  3579  2reurex  3721  2reu1  3849  rexdifi  4089  r19.2z  4458  falseral0OLD  4474  elelpwi  4570  preqsnd  4819  prproe  4838  ssuni  4898  disji2  5092  disjiun  5096  disjxiun  5105  trintss  5237  ssexgOLD  5292  reusv2lem3  5369  propeqop  5486  otiunsndisj  5500  rexopabb  5509  pofun  5584  solin  5593  2optocl  5755  3optocl  5756  ssrelrn  5888  elrnmpt1  5954  resieq  5997  imadifssranOLDOLD  6222  welb  6317  reuop  6322  fnun  6683  fss  6756  fun  6774  fvelimab  6988  fvmptss  7037  fvn0ssdmfun  7106  fvcofneq  7125  fmptco  7162  funsndifnop  7187  fnressn  7194  fressnfv  7196  fmptsng  7204  fvtp2g  7235  fvtp3g  7236  tpres  7238  fnex  7254  funfvima3  7273  fvf1pr  7346  isores3  7374  tfisg  7899  dmfex  7951  opreuopreu  8080  releldmdifi  8091  funeldmdif  8094  el2mpocsbcl  8131  f1o2ndf1  8170  frxp  8175  fnse  8187  frxp2  8198  frxp3  8205  poseq  8212  ressuppssdif  8240  funsssuppss  8245  mpoxopxnop0  8270  reldmtpos  8289  frrlem8  8349  fpr2a  8358  smores  8398  tfrlem7  8429  onelfvnef1  8487  tz7.48-2  8490  tz7.49  8493  oacl  8581  omcl  8582  oecl  8583  oarec  8608  oewordri  8639  oeworde  8640  oelim2  8642  oeoa  8644  oeoelem  8645  oeoe  8646  nnacl  8658  nnmcl  8659  nnecl  8660  nnmsucr  8672  naddoa  8750  brinxper  8785  2ecoptocl  8867  fsetprcnex  8922  undifixp  9000  funen1cnv  9094  xpf1o  9196  limensuc  9211  unfi  9224  en1eqsn  9304  ac6sfi  9313  frfi  9314  difinf  9341  f1dmvrnfibi  9368  f1vrnfibi  9369  suppeqfsuppbi  9408  elfiun  9459  dffi3  9460  infsupprpr  9535  xpwdomg  9616  infdiffi  9696  ttrclselem2  9764  epfrs  9769  frmin  9790  frr2  9801  rankxpsuc  9936  rankfilimbi  9939  r1filimi  9940  updjud  10052  tskwe  10068  infxpenlem  10131  fseqenlem1  10142  kmlem2  10269  nnadju  10315  cff1  10375  cflim2  10380  sornom  10394  infpssrlem4  10423  fin23lem26  10442  fin23lem30  10459  fin23lem34  10463  isf32lem11  10480  fin67  10512  isfin7-2  10513  fin1a2lem10  10526  axcc2lem  10553  axdc2lem  10565  axdc3lem2  10568  axdc3lem4  10570  axdc4lem  10572  iunfo  10662  tsk0  10887  gruina  10942  grur1a  10943  mulcanenq  11084  reclem2pr  11172  supsrlem  11235  supsr  11236  ax1rid  11285  negf1o  11785  lbreu  12307  nnindd  12395  nnaddcl  12398  nnmulcl  12399  nn0n0n1ge2b  12715  nn0indd  12836  fzind  12837  fnn0ind  12838  uzaddcl  13071  uzinfi  13095  nn01to3  13108  elpq  13143  xmulasslem2  13452  supxrunb1  13489  supxrunb2  13490  infmremnf  13514  infmrp1  13515  uzsubsubfz  13720  fzdif1  13779  elfz0ubfz0  13806  fz0fzdiffz0  13811  elfzmlbp  13813  fzofzim  13884  elfzom1elp1fzo  13907  ssfzo12bi  13936  fzoopth  13937  fzonfzoufzol  13946  elfznelfzob  13949  injresinjlem  13965  injresinj  13966  modaddmodup  14117  modfzo0difsn  14126  modsumfzodifsn  14127  addmodlteq  14129  om2uzlti  14133  fsequb  14158  ssnn0fi  14168  ser1const  14241  expcllem  14255  expeq0  14275  expmordi  14350  expnngt1  14426  faclbnd  14475  hashf1rn  14537  hashgadd  14562  hashunx  14571  hashnn0n0nn  14576  hashgt0elex  14586  hashss  14594  hashfzp1  14617  hashxp  14620  hashmap  14621  hashimarni  14627  seqcoll  14650  hash2exprb  14657  hashge2el2difr  14667  elss2prb  14674  hashdifsnp1  14692  fi1uzind  14693  brfi1indALT  14696  lswlgt0cl  14755  swrdnd  14846  swrdnnn0nd  14848  swrdnd0  14849  swrd0  14850  swrdsbslen  14856  swrdspsleq  14857  pfxsuff1eqwrdeq  14890  swrdswrdlem  14895  swrdswrd  14896  wrd2ind  14914  pfxccatin12lem2a  14918  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccatin12lem3  14923  pfxccatin12  14924  pfxccat3  14925  swrdccat  14926  pfxccat3a  14929  swrdccat3blem  14930  repswswrd  14977  repswrevw  14980  cshwmodn  14988  cshwsublen  14989  cshwidxmod  14996  cshwidxmodr  14997  cshf1  15003  2cshw  15006  cshweqrep  15014  cshw1  15015  2cshwcshw  15018  cshwcshid  15020  cshwcsh2id  15021  wrdlen2i  15136  2swrd2eqwrdeq  15149  wwlktovfo  15154  relexpsucnnl  15226  rtrclreclem3  15256  rtrclreclem4  15257  relexpindlem  15259  r19.29uz  15562  caubnd  15570  sqreu  15572  climshft  15787  climub  15873  climserle  15874  sumss  15934  sumss2  15936  modfsummods  16004  o1fsum  16024  binom  16043  climcndslem1  16062  climcndslem2  16063  cvgrat  16096  clim2prod  16101  prodfn0  16107  prodfrec  16108  ntrivcvgfvn0  16112  fprodn0  16190  fprodmodd  16208  fprodefsum  16305  demoivreALT  16413  ruclem8  16449  dvdsaddre2b  16521  dvdsdivcl  16530  dvdsfac  16540  oddnn02np1  16562  oddge22np1  16563  evennn02n  16564  evennn2n  16565  m1exp1  16590  nn0o  16597  pwp1fsum  16605  flodddiv4  16629  smu01lem  16699  dvdslegcd  16718  gcdneg  16738  dfgcd2  16763  seq1st  16790  alginv  16794  lcmf  16852  lcmftp  16855  lcmfunsnlem2lem2  16858  lcmfunsnlem  16860  lcmfun  16864  ncoprmgcdne1b  16869  coprmproddvdslem  16881  coprmproddvds  16882  cncongr1  16886  prmdvdsexp  16935  prmndvdsfaclt  16945  ncoprmlnprm  16948  fvprmselgcd1  17267  prmgaplem6  17278  prmgaplem7  17279  prmgaplem8  17280  cshwshashlem1  17317  setsstruct2  17396  setsstruct  17398  inveq  17999  catsubcat  18064  initoeu2lem0  18238  initoeu2lem1  18239  funcestrcsetclem8  18371  funcestrcsetclem9  18372  fthestrcsetc  18374  fullestrcsetc  18375  funcsetcestrclem9  18387  fthsetcestrc  18389  fullsetcestrc  18390  lubss  18737  lubel  18738  mgmpropd  18879  issstrmgm  18881  mgmb1mgm1  18883  mgmidpfod  18907  frmdgsum  19108  smndex1mndlem  19158  mgm2nsgrplem3  19169  dfgrp2  19223  cyccom  19468  gaass  19562  gsumwrev  19631  symgextf1lem  19685  symgextf1  19686  fvcosymgeq  19694  gsmsymgreq  19697  symgfixelsi  19700  pmtrprfv3  19719  symggen  19735  pmtrprfval  19752  gsumzres  20174  gsumpr  20220  gsumzunsnd  20221  srgmulgass  20494  srgbinom  20508  0ringnnzr  20827  rnghmsscmap  20933  rnghmsubcsetclem2  20935  rngcinv  20940  funcrngcsetc  20943  funcrngcsetcALT  20944  rhmsscmap  20962  rhmsubcsetclem2  20964  rhmsubcrngclem2  20970  funcringcsetc  20977  srhmsubc  20983  rhmsubclem4  20991  lmodvsmmulgdi  21223  lmodfopnelem1  21224  rmodislmodlem  21255  rngqiprngimfo  21648  cnfldmulg  21762  cnfldexp  21763  ofldchr  21937  psgndiflemB  21961  assamulgscm  22264  gsumply1subr  22606  gsummoncoe1  22681  pf1ind  22728  matmulcell  22815  mat1dimscm  22845  dmatmul  22867  dmatscmcl  22873  scmataddcl  22886  scmatsubcl  22887  scmatsgrp1  22892  mavmulsolcl  22921  ma1repveval  22941  1marepvmarrepid  22945  symgmatr01lem  23023  matunitlindf  23051  slesolvec  23052  cramerimplem2  23057  decpmatmullem  23144  pm2mpf1  23172  mp2pm2mplem4  23182  monmat2matmon  23197  chpscmat  23215  chpscmatgsumbin  23217  fvmptnn04ifb  23224  chfacfscmul0  23231  chfacfscmulgsum  23233  chfacfpmmul0  23235  chfacfpmmulgsum  23237  cpmadugsumlemF  23249  toprntopon  23298  clsss  23427  ntrss  23428  restntr  23555  cmpsublem  23772  cmpsub  23773  2ndcrest  23827  txindislem  24007  t0kq  24192  filufint  24294  fbflim2  24351  flftg  24370  alexsubALTlem4  24424  cnextfvval  24439  ustuqtop4  24618  xmettri2  24714  mettri  24726  metss  24882  tngngp3  25030  clmvscom  25466  lmmbr  25634  caublcls  25685  lmcau  25689  ovolunlem1a  25872  nulmbl2  25912  voliunlem1  25926  iunmbl  25929  volsup  25932  dvlip  26368  dvfsumle  26396  degltlem1  26445  ply1divex  26510  plyco  26615  dgrnznn  26621  dvnply2  26663  plydivex  26673  aannenlem2  26713  aaliou3lem2  26727  ulmcau  26779  zabsle1  27680  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  gausslemma2dlem3  27752  gausslemma2dlem4  27753  2lgslem1a1  27773  2sqnn0  27822  2sqreulem1  27830  2sqreunnlem1  27833  dchrisumlem1  27873  dchrisumlem2  27874  dchrisumlem3  27875  qabvle  28009  ostthlem2  28012  ostth2lem2  28018  nosupbnd1lem5  28126  noinfbnd1lem5  28141  nocvxminlem  28197  lesrec  28242  madebdaylemold  28341  mulsuniflem  28592  precsexlem6  28655  precsexlem7  28656  precsexlem8  28657  precsexlem9  28658  abssge0  28688  noseqind  28735  om2noseqlt  28742  om2noseqrdg  28747  n0addscl  28787  n0mulscl  28788  onsfi  28799  oldfib  28820  expscllem  28873  pw2cut2  28905  z12zsodd  28925  tgjustr  28993  axeuclidlem  29597  incistruhgr  29714  umgredgprv  29742  umgrpredgv  29775  usgredgprvALT  29833  uhgr2edg  29846  usgredg2vlem2  29864  lfuhgr1v0e  29892  subgrfun  29919  umgrres1lem  29948  upgrres1  29951  fusgrfis  29968  uhgrnbgr0nb  29992  nbgr1vtx  29996  nb3grprlem1  30018  uvtx01vtx  30035  fusgrn0degnn0  30137  vtxdginducedm1lem4  30180  finsumvtxdg2size  30188  wlkl1loop  30275  wlkres  30306  lfgrwlknloop  30329  pthdadjvtx  30370  dfpth2  30371  upgr2pthnlp  30375  upgrwlkdvdelem  30379  upgrwlkdvde  30380  uhgrwkspthlem2  30397  usgr2trlspth  30404  usgr2pth  30407  pthdlem2lem  30410  cyclnumvtx  30445  lfgrn1cycl  30451  uspgrn2crct  30454  crctcshwlkn0lem3  30458  crctcshwlkn0lem4  30459  crctcshwlkn0lem5  30460  iswspthsnon  30502  wlkiswwlks1  30513  wlklnwwlkln1  30514  wlkiswwlks2  30521  wlkiswwlksupgr2  30523  wlklnwwlkln2lem  30528  wlknwwlksnbij  30534  wwlksnred  30538  wwlksnext  30539  wwlksnredwwlkn  30541  wwlksnredwwlkn0  30542  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextsurj  30546  wspthsnonn0vne  30563  wspn0  30570  wwlks2onv  30599  elwwlks2  30615  elwspths2spth  30616  rusgrnumwwlk  30624  clwwlkccatlem  30637  clwlkclwwlklem2a1  30640  clwlkclwwlklem2fv2  30644  clwlkclwwlklem2a4  30645  clwlkclwwlklem2a  30646  clwlkclwwlklem2  30648  clwlkclwwlkf1lem3  30654  clwwisshclwwslem  30662  clwwisshclwwsn  30664  erclwwlktr  30670  isclwwlknx  30684  clwwlkinwwlk  30688  clwwlkel  30694  clwwlkf  30695  clwwlkf1  30697  clwwlkfo  30698  clwwlkext2edg  30704  wwlksext2clwwlk  30705  wwlksubclwwlk  30706  clwwlknscsh  30710  erclwwlkntr  30719  eleclclwwlkn  30724  hashecclwwlkn1  30725  umgrhashecclwwlk  30726  clwwlknon0  30741  clwwlknonel  30743  clwwlknon1  30745  clwwlknonwwlknonb  30754  clwwlknonex2lem2  30756  clwwlknun  30760  clwwlkvbij  30761  upgr3v3e3cycl  30838  uhgr3cyclex  30840  upgr4cycl4dv4e  30843  eulerpath  30899  eucrctshift  30901  eucrct2eupth  30903  1to2vfriswmgr  30937  1to3vfriswmgr  30938  3cyclfrgrrn1  30943  4cycl2vnunb  30948  frgrwopreglem2  30971  frgrwopreglem3  30972  frgrwopreglem5ALT  30980  fusgr2wsp2nb  30992  2clwwlk2clwwlklem  31004  2clwwlk2clwwlk  31008  numclwwlk1lem2f1  31015  numclwwlk1lem2fo  31016  numclwwlk1  31019  clwwlknonclwlknonf1o  31020  dlwwlknondlwlknonf1o  31023  numclwlk1  31029  numclwlk2lem2f  31035  numclwlk2lem2f1o  31037  numclwwlk5  31046  frgrreg  31052  frgrregord013  31053  friendship  31057  nsnlplig  31140  nsnlpligALT  31141  isgrpo  31156  vcdi  31224  vcdir  31225  vcass  31226  nmosetre  31423  hlim2  31851  shscli  31976  chintcli  31990  dfch2  32066  spansncvi  32311  nmopsetretALT  32522  nmfnsetre  32536  lnopl  32573  lnfnl  32590  pjss2coi  32823  pjorthcoi  32828  pjscji  32829  pjssdif2i  32833  pjclem4a  32857  pj3lem1  32865  strlem5  32914  hstrlem5  32922  cvmdi  32983  mdslmd3i  32991  atcv1  33039  atcvat4i  33056  cdj3lem2a  33095  cdj3lem3a  33098  opreu2reuALT  33172  iuninc  33253  disji2f  33269  disjif2  33273  fmptcof2  33349  xrsmulgzz  33669  1arithufdlem3  34182  esumfzf  34812  issgon  34866  voliune  34973  volfiniune  34974  rrvsum  35197  bnj228  35477  bnj1294  35558  bnj229  35625  bnj607  35657  bnj908  35672  bnj953  35680  bnj1118  35725  bnj1174  35744  bnj1388  35774  trssfihf  35860  trssfihfregs  35945  prconf1acwevd  36089  acycgrsubgr  36121  cvmliftlem15  36271  satfsschain  36337  satfdm  36342  satf0op  36350  fmla0xp  36356  gonarlem  36367  goalrlem  36369  satffunlem1lem1  36375  satffunlem2lem1  36377  dmopab3rexdif  36378  satefvfmla0  36391  prv1n  36404  iprodefisumlem  36720  faclimlem1  36723  dfon2lem6  36765  idinside  37064  onsucconni  37440  axuntco  37482  ttcmin  37499  elttctr  37508  dfttc2g  37509  bj-cbvew  37756  axc11n11r  37800  comodular  38207  bj-brrelex12ALT  38252  bj-snmoore  38304  bj-finsumval0  38474  exlimim  38533  exellim  38535  icoreclin  38548  difunieq  38565  fvineqsneq  38603  pibt2  38608  wl-spae  38721  wl-aleq  38735  fin2so  38798  poimirlem4  38810  poimirlem26  38832  itg2addnclem  38857  upixp  38931  sdclem2  38942  metf1o  38955  sstotbnd3  38976  isbndx  38982  ismtycnv  39002  heiborlem4  39014  bfplem1  39022  opidonOLD  39052  grpomndo  39075  eldisjdmqsim2  40014  ax12eq  40264  ax12el  40265  cvrat4  40766  nn0addcom  43792  nn0mulcom  43796  mzpexpmpt  44022  diophren  44086  rmxypos  44220  jm2.17a  44233  jm2.17b  44234  rmygeid  44237  jm2.18  44261  jm2.25  44272  jm2.15nn0  44276  jm2.16nn0  44277  pwslnm  44362  isnumbasgrplem1  44368  dgraalem  44412  onuniintrab  44489  onsupuni  44492  onsupcl3  44496  naddonnn  44658  naddwordnexlem2  44661  relexpiidm  44965  relexpmulnn  44970  relexpmulg  44971  relexp01min  44974  relexp0a  44977  relexpxpmin  44978  clsk1indlem3  45304  grucollcld  45505  dvgrat  45557  radcnvrat  45559  sspwimpcf  46162  sspwimpcfVD  46163  e2ebindALT  46171  trfr  46216  et-sqrtnegnre  48156  fsetprcnexALT  48405  aiotaexim  48441  eu2ndop1stv  48468  afvfv0bi  48495  afveu  48496  afvres  48515  aovmpt4g  48544  ndmaovass  48549  ndmaovdistr  48550  afv2orxorb  48571  afv2eu  48581  imarnf1pr  48625  nltle2tri  48656  fzopredsuc  48667  subsubelfzo0  48670  2ffzoeq  48671  2tceilhalfelfzo1  48679  m1modmmod  48707  smonoord  48720  elsetpreimafvssdm  48741  iccpartres  48773  iccpartiltu  48777  iccpartigtl  48778  iccpartgt  48782  icceuelpartlem  48790  fargshiftf1  48796  ichnreuop  48827  ichreuopeq  48828  elsprel  48830  sprsymrelfo  48852  prproropf1olem4  48861  paireqne  48866  sbcpr  48876  reupr  48877  goldbachth  48905  fmtnoprmfac1  48923  fmtnoprmfac2  48925  prmdvdsfmtnof1lem2  48943  lighneallem2  48964  lighneallem4  48968  requad2  48994  even3prm2  49090  fpprwpprb  49111  gbegt5  49132  sbgoldbwt  49148  sbgoldbm  49155  nnsum3primesgbe  49163  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  bgoldbtbnd  49180  isubgredg  49237  grimuhgr  49258  clnbgrgrim  49305  grtriprop  49312  cycl3grtrilem  49317  cycl3grtri  49318  gpgusgralem  49427  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgcubic  49450  gpg5nbgr3star  49452  gpgprismgr4cycllem3  49468  upgrwlkupwlk  49511  uspgropssxp  49515  uspgrsprfo  49519  isassintop  49580  lidldomn1  49601  2zlidl  49610  2zrngamgm  49615  2zrngmmgm  49622  rngccatidALTV  49642  rngcinvALTV  49646  rhmsubcALTVlem4  49654  funcringcsetcALTV2lem9  49668  ringccatidALTV  49676  srhmsubcALTV  49695  lmodvsmdi  49822  ply1mulgsumlem1  49829  ply1mulgsumlem2  49830  lincdifsn  49867  lincsumcl  49874  lincscmcl  49875  lincext3  49899  lindslinindsimp1  49900  lindslinindsimp2lem5  49905  snlindsntor  49914  lincresunit2  49921  lincresunit3lem2  49923  zgtp1leeq  49964  elbigo2  49995  fllog2  50011  digexp  50050  dig1  50051  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063  1arymaptf1  50085  2arymaptf1  50096  rrxlinec  50180  rrx2linest  50185  itsclc0yqsol  50207  itsclc0xyqsol  50211