Theorem impcom 412

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpan9  515  anbiim  652  bianir  1072  19.29r  1901  19.41v  1976  19.41  2277  nfsb4t  2537  mo4  2600  2euexv  2665  2euex  2675  gencl  3504  2gencl  3505  vtocl2ga  3551  vtocl2gaf  3552  vtocl3gaf  3553  vtocl3ga  3554  vtocl4g  3555  vtocl4ga  3556  rspccva  3589  2reurex  3732  2reu1  3859  rexdifi  4112  sseq0  4367  r19.2z  4465  falseral0OLD  4481  elelpwi  4577  preqsnd  4828  prproe  4874  ssuni  4902  disji2  5097  disjiun  5101  disjxiun  5110  trintss  5241  ssexg  5294  reusv2lem3  5372  propeqop  5491  otiunsndisj  5504  rexopabb  5513  pofun  5588  solin  5597  2optocl  5758  3optocl  5759  ssrelrn  5885  elrnmpt1  5951  resieq  5990  imadifssranOLD  6204  reuop  6295  fnun  6650  fss  6723  fun  6741  fvelimab  6954  fvmptss  7003  fvn0ssdmfun  7070  fvcofneq  7089  fmptco  7126  funsndifnop  7149  fnressn  7156  fressnfv  7158  fmptsng  7167  fvtp2g  7198  fvtp3g  7199  tpres  7200  fnex  7216  funfvima3  7235  fvf1pr  7306  isores3  7334  tfisg  7849  dmfex  7901  opreuopreu  8030  releldmdifi  8041  funeldmdif  8044  el2mpocsbcl  8079  f1o2ndf1  8116  frxp  8121  fnse  8128  frxp2  8139  frxp3  8146  poseq  8153  ressuppssdif  8180  funsssuppss  8185  mpoxopxnop0  8210  reldmtpos  8229  frrlem8  8289  fpr2a  8298  smores  8338  tfrlem7  8369  tz7.48-2  8428  tz7.49  8431  oacl  8519  omcl  8520  oecl  8521  oarec  8546  oewordri  8577  oeworde  8578  oelim2  8580  oeoa  8582  oeoelem  8583  oeoe  8584  nnacl  8596  nnmcl  8597  nnecl  8598  nnmsucr  8610  naddoa  8688  brinxper  8723  2ecoptocl  8805  fsetprcnex  8858  undifixp  8931  xpf1o  9126  limensuc  9141  unfi  9154  en1eqsn  9234  ac6sfi  9243  frfi  9244  difinf  9270  f1dmvrnfibi  9297  f1vrnfibi  9298  suppeqfsuppbi  9338  elfiun  9389  dffi3  9390  infsupprpr  9465  xpwdomg  9546  infdiffi  9626  ttrclselem2  9694  epfrs  9699  frmin  9720  frr2  9731  rankxpsuc  9853  updjud  9919  tskwe  9935  infxpenlem  9996  fseqenlem1  10007  kmlem2  10134  nnadju  10180  cff1  10241  cflim2  10246  sornom  10260  infpssrlem4  10289  fin23lem26  10308  fin23lem30  10325  fin23lem34  10329  isf32lem11  10346  fin67  10378  isfin7-2  10379  fin1a2lem10  10392  axcc2lem  10419  axdc2lem  10431  axdc3lem2  10434  axdc3lem4  10436  axdc4lem  10438  iunfo  10522  tsk0  10747  gruina  10802  grur1a  10803  mulcanenq  10944  reclem2pr  11032  supsrlem  11095  supsr  11096  ax1rid  11145  negf1o  11643  lbreu  12164  nnindd  12252  nnaddcl  12255  nnmulcl  12256  nn0n0n1ge2b  12572  nn0indd  12692  fzind  12693  fnn0ind  12694  uzaddcl  12927  uzinfi  12951  nn01to3  12964  elpq  12998  xmulasslem2  13307  supxrunb1  13344  supxrunb2  13345  infmremnf  13369  infmrp1  13370  uzsubsubfz  13573  fzdif1  13632  elfz0ubfz0  13659  fz0fzdiffz0  13664  elfzmlbp  13666  fzofzim  13737  elfzom1elp1fzo  13760  ssfzo12bi  13789  fzoopth  13790  fzonfzoufzol  13799  elfznelfzob  13802  injresinjlem  13818  injresinj  13819  modaddmodup  13969  modfzo0difsn  13978  modsumfzodifsn  13979  addmodlteq  13981  om2uzlti  13985  fsequb  14010  ssnn0fi  14020  ser1const  14093  expcllem  14107  expeq0  14127  expmordi  14202  expnngt1  14276  faclbnd  14325  hashf1rn  14387  hashgadd  14412  hashunx  14421  hashnn0n0nn  14426  hashgt0elex  14436  hashss  14444  hashfzp1  14467  hashxp  14470  hashmap  14471  hashimarni  14477  seqcoll  14500  hash2exprb  14507  hashge2el2difr  14517  elss2prb  14524  hashdifsnp1  14542  fi1uzind  14543  brfi1indALT  14546  lswlgt0cl  14605  swrdnd  14691  swrdnnn0nd  14693  swrdnd0  14694  swrd0  14695  swrdsbslen  14701  swrdspsleq  14702  pfxsuff1eqwrdeq  14735  swrdswrdlem  14740  swrdswrd  14741  wrd2ind  14759  pfxccatin12lem2a  14763  swrdccatin2  14765  pfxccatin12lem2  14767  pfxccatin12lem3  14768  pfxccatin12  14769  pfxccat3  14770  swrdccat  14771  pfxccat3a  14774  swrdccat3blem  14775  repswswrd  14820  repswrevw  14823  cshwmodn  14831  cshwsublen  14832  cshwidxmod  14839  cshwidxmodr  14840  cshf1  14846  2cshw  14849  cshweqrep  14857  cshw1  14858  2cshwcshw  14861  cshwcshid  14863  cshwcsh2id  14864  wrdlen2i  14978  2swrd2eqwrdeq  14989  wwlktovfo  14994  relexpsucnnl  15066  rtrclreclem3  15096  rtrclreclem4  15097  relexpindlem  15099  r19.29uz  15401  caubnd  15409  sqreu  15411  climshft  15626  climub  15712  climserle  15713  sumss  15774  sumss2  15776  modfsummods  15844  o1fsum  15864  binom  15883  climcndslem1  15902  climcndslem2  15903  cvgrat  15936  clim2prod  15941  prodfn0  15947  prodfrec  15948  ntrivcvgfvn0  15952  fprodn0  16032  fprodmodd  16050  fprodefsum  16148  demoivreALT  16256  ruclem8  16292  dvdsaddre2b  16364  dvdsdivcl  16373  dvdsfac  16383  oddnn02np1  16405  oddge22np1  16406  evennn02n  16407  evennn2n  16408  m1exp1  16433  nn0o  16440  pwp1fsum  16448  flodddiv4  16472  smu01lem  16542  dvdslegcd  16561  gcdneg  16579  dfgcd2  16603  seq1st  16628  alginv  16632  lcmf  16690  lcmftp  16693  lcmfunsnlem2lem2  16696  lcmfunsnlem  16698  lcmfun  16702  ncoprmgcdne1b  16707  coprmproddvdslem  16719  coprmproddvds  16720  cncongr1  16724  prmdvdsexp  16773  prmndvdsfaclt  16783  ncoprmlnprm  16786  fvprmselgcd1  17104  prmgaplem6  17115  prmgaplem7  17116  prmgaplem8  17117  cshwshashlem1  17154  setsstruct2  17233  setsstruct  17235  inveq  17830  catsubcat  17895  initoeu2lem0  18069  initoeu2lem1  18070  funcestrcsetclem8  18202  funcestrcsetclem9  18203  fthestrcsetc  18205  fullestrcsetc  18206  funcsetcestrclem9  18218  fthsetcestrc  18220  fullsetcestrc  18221  lubss  18568  lubel  18569  mgmpropd  18708  issstrmgm  18710  mgmb1mgm1  18712  sgrpidmnd  18796  frmdgsum  18920  smndex1mndlem  18970  mgm2nsgrplem3  18981  dfgrp2  19028  cyccom  19273  gaass  19366  gsumwrev  19435  symgextf1lem  19489  symgextf1  19490  fvcosymgeq  19498  gsmsymgreq  19501  symgfixelsi  19504  pmtrprfv3  19523  symggen  19539  pmtrprfval  19556  gsumzres  19978  gsumpr  20024  gsumzunsnd  20025  srgmulgass  20298  srgbinom  20312  0ringnnzr  20608  rnghmsscmap  20714  rnghmsubcsetclem2  20716  rngcinv  20721  funcrngcsetc  20724  funcrngcsetcALT  20725  rhmsscmap  20743  rhmsubcsetclem2  20745  rhmsubcrngclem2  20751  funcringcsetc  20758  srhmsubc  20764  rhmsubclem4  20772  lmodvsmmulgdi  20995  lmodfopnelem1  20996  rmodislmodlem  21027  rngqiprngimfo  21411  cnfldmulg  21522  cnfldexp  21523  ofldchr  21694  psgndiflemB  21718  assamulgscm  22019  gsumply1subr  22361  gsummoncoe1  22436  pf1ind  22483  matmulcell  22570  mat1dimscm  22600  dmatmul  22622  dmatscmcl  22628  scmataddcl  22641  scmatsubcl  22642  scmatsgrp1  22647  mavmulsolcl  22676  ma1repveval  22696  1marepvmarrepid  22700  symgmatr01lem  22778  slesolvec  22804  cramerimplem2  22809  decpmatmullem  22896  pm2mpf1  22924  mp2pm2mplem4  22934  monmat2matmon  22949  chpscmat  22967  chpscmatgsumbin  22969  fvmptnn04ifb  22976  chfacfscmul0  22983  chfacfscmulgsum  22985  chfacfpmmul0  22987  chfacfpmmulgsum  22989  cpmadugsumlemF  23001  toprntopon  23050  clsss  23179  ntrss  23180  restntr  23307  cmpsublem  23524  cmpsub  23525  2ndcrest  23579  txindislem  23758  t0kq  23943  filufint  24045  fbflim2  24102  flftg  24121  alexsubALTlem4  24175  cnextfvval  24190  ustuqtop4  24369  xmettri2  24465  mettri  24477  metss  24633  tngngp3  24781  clmvscom  25217  lmmbr  25385  caublcls  25436  lmcau  25440  ovolunlem1a  25623  nulmbl2  25663  voliunlem1  25677  iunmbl  25680  volsup  25683  dvlip  26120  dvfsumle  26148  degltlem1  26197  ply1divex  26262  plyco  26366  dgrnznn  26372  dvnply2  26416  plydivex  26426  aannenlem2  26458  aaliou3lem2  26472  ulmcau  26523  zabsle1  27425  gausslemma2dlem1a  27494  gausslemma2dlem2  27496  gausslemma2dlem3  27497  gausslemma2dlem4  27498  2lgslem1a1  27518  2sqnn0  27567  2sqreulem1  27575  2sqreunnlem1  27578  dchrisumlem1  27618  dchrisumlem2  27619  dchrisumlem3  27620  qabvle  27754  ostthlem2  27757  ostth2lem2  27763  nosupbnd1lem5  27841  noinfbnd1lem5  27856  nocvxminlem  27912  lesrec  27957  madebdaylemold  28056  mulsuniflem  28307  precsexlem6  28370  precsexlem7  28371  precsexlem8  28372  precsexlem9  28373  abssge0  28403  noseqind  28450  om2noseqlt  28457  om2noseqrdg  28462  n0addscl  28502  n0mulscl  28503  onsfi  28514  oldfib  28535  expscllem  28588  pw2cut2  28620  z12zsodd  28640  tgjustr  28708  axeuclidlem  29252  incistruhgr  29369  umgredgprv  29397  umgrpredgv  29430  usgredgprvALT  29485  uhgr2edg  29498  usgredg2vlem2  29516  lfuhgr1v0e  29544  subgrfun  29571  umgrres1lem  29600  upgrres1  29603  fusgrfis  29620  uhgrnbgr0nb  29644  nbgr1vtx  29648  nb3grprlem1  29670  uvtx01vtx  29687  fusgrn0degnn0  29789  vtxdginducedm1lem4  29832  finsumvtxdg2size  29840  wlkl1loop  29927  wlkres  29958  lfgrwlknloop  29977  pthdadjvtx  30017  dfpth2  30018  upgr2pthnlp  30021  upgrwlkdvdelem  30025  upgrwlkdvde  30026  uhgrwkspthlem2  30043  usgr2trlspth  30050  usgr2pth  30053  pthdlem2lem  30056  cyclnumvtx  30089  lfgrn1cycl  30094  uspgrn2crct  30097  crctcshwlkn0lem3  30101  crctcshwlkn0lem4  30102  crctcshwlkn0lem5  30103  iswspthsnon  30145  wlkiswwlks1  30156  wlklnwwlkln1  30157  wlkiswwlks2  30164  wlkiswwlksupgr2  30166  wlklnwwlkln2lem  30171  wlknwwlksnbij  30177  wwlksnred  30181  wwlksnext  30182  wwlksnredwwlkn  30184  wwlksnredwwlkn0  30185  wwlksnextfun  30187  wwlksnextinj  30188  wwlksnextsurj  30189  wspthsnonn0vne  30206  wspn0  30213  wwlks2onv  30242  elwwlks2  30258  elwspths2spth  30259  rusgrnumwwlk  30267  clwwlkccatlem  30280  clwlkclwwlklem2a1  30283  clwlkclwwlklem2fv2  30287  clwlkclwwlklem2a4  30288  clwlkclwwlklem2a  30289  clwlkclwwlklem2  30291  clwlkclwwlkf1lem3  30297  clwwisshclwwslem  30305  clwwisshclwwsn  30307  erclwwlktr  30313  isclwwlknx  30327  clwwlkinwwlk  30331  clwwlkel  30337  clwwlkf  30338  clwwlkf1  30340  clwwlkfo  30341  clwwlkext2edg  30347  wwlksext2clwwlk  30348  wwlksubclwwlk  30349  clwwlknscsh  30353  erclwwlkntr  30362  eleclclwwlkn  30367  hashecclwwlkn1  30368  umgrhashecclwwlk  30369  clwwlknon0  30384  clwwlknonel  30386  clwwlknon1  30388  clwwlknonwwlknonb  30397  clwwlknonex2lem2  30399  clwwlknun  30403  clwwlkvbij  30404  upgr3v3e3cycl  30471  uhgr3cyclex  30473  upgr4cycl4dv4e  30476  eulerpath  30532  eucrctshift  30534  eucrct2eupth  30536  1to2vfriswmgr  30570  1to3vfriswmgr  30571  3cyclfrgrrn1  30576  4cycl2vnunb  30581  frgrwopreglem2  30604  frgrwopreglem3  30605  frgrwopreglem5ALT  30613  fusgr2wsp2nb  30625  2clwwlk2clwwlklem  30637  2clwwlk2clwwlk  30641  numclwwlk1lem2f1  30648  numclwwlk1lem2fo  30649  numclwwlk1  30652  clwwlknonclwlknonf1o  30653  dlwwlknondlwlknonf1o  30656  numclwlk1  30662  numclwlk2lem2f  30668  numclwlk2lem2f1o  30670  numclwwlk5  30679  frgrreg  30685  frgrregord013  30686  friendship  30690  nsnlplig  30773  nsnlpligALT  30774  isgrpo  30789  vcdi  30857  vcdir  30858  vcass  30859  nmosetre  31056  hlim2  31484  shscli  31609  chintcli  31623  dfch2  31699  spansncvi  31944  nmopsetretALT  32155  nmfnsetre  32169  lnopl  32206  lnfnl  32223  pjss2coi  32456  pjorthcoi  32461  pjscji  32462  pjssdif2i  32466  pjclem4a  32490  pj3lem1  32498  strlem5  32547  hstrlem5  32555  cvmdi  32616  mdslmd3i  32624  atcv1  32672  atcvat4i  32689  cdj3lem2a  32728  cdj3lem3a  32731  opreu2reuALT  32763  iuninc  32845  disji2f  32862  disjif2  32866  fmptcof2  32942  xrsmulgzz  33269  1arithufdlem3  33780  esumfzf  34403  issgon  34457  voliune  34563  volfiniune  34564  rrvsum  34788  bnj228  35068  bnj1294  35149  bnj229  35216  bnj607  35248  bnj908  35263  bnj953  35271  bnj1118  35316  bnj1174  35335  bnj1388  35365  funen1cnv  35419  rankfilimbi  35436  r1filimi  35438  trssfir1om  35446  trssfir1omregs  35471  acycgrsubgr  35548  cvmliftlem15  35688  satfsschain  35754  satfdm  35759  satf0op  35767  fmla0xp  35773  gonarlem  35784  goalrlem  35786  satffunlem1lem1  35792  satffunlem2lem1  35794  dmopab3rexdif  35795  satefvfmla0  35808  prv1n  35821  iprodefisumlem  36130  faclimlem1  36133  dfon2lem6  36176  idinside  36474  onsucconni  36836  axuntco  36878  ttcmin  36895  elttctr  36904  dfttc2g  36905  mh-inf3f1  36940  bj-cbvew  37152  axc11n11r  37196  bj-brrelex12ALT  37590  bj-snmoore  37642  bj-finsumval0  37816  exlimim  37875  exellim  37877  icoreclin  37890  difunieq  37907  fvineqsneq  37945  pibt2  37950  wl-spae  38063  wl-aleq  38077  fin2so  38145  matunitlindf  38156  poimirlem4  38162  poimirlem26  38184  itg2addnclem  38209  upixp  38267  welb  38274  sdclem2  38280  metf1o  38293  sstotbnd3  38314  isbndx  38320  ismtycnv  38340  heiborlem4  38352  bfplem1  38360  opidonOLD  38390  grpomndo  38413  eldisjdmqsim2  39354  ax12eq  39604  ax12el  39605  cvrat4  40106  nn0addcom  43125  nn0mulcom  43129  mzpexpmpt  43367  diophren  43431  rmxypos  43565  jm2.17a  43578  jm2.17b  43579  rmygeid  43582  jm2.18  43606  jm2.25  43617  jm2.15nn0  43621  jm2.16nn0  43622  pwslnm  43712  isnumbasgrplem1  43719  dgraalem  43763  onuniintrab  43844  onsupuni  43847  onsupcl3  43851  naddonnn  44013  naddwordnexlem2  44016  relexpiidm  44321  relexpmulnn  44326  relexpmulg  44327  relexp01min  44330  relexp0a  44333  relexpxpmin  44334  clsk1indlem3  44660  grucollcld  44861  dvgrat  44913  radcnvrat  44915  sspwimpcf  45519  sspwimpcfVD  45520  e2ebindALT  45528  trfr  45562  et-sqrtnegnre  47478  fsetprcnexALT  47687  eu2ndop1stv  47750  afvfv0bi  47777  afveu  47778  afvres  47797  aovmpt4g  47826  ndmaovass  47831  ndmaovdistr  47832  afv2orxorb  47853  afv2eu  47863  imarnf1pr  47907  nltle2tri  47938  fzopredsuc  47949  subsubelfzo0  47952  2ffzoeq  47953  2tceilhalfelfzo1  47961  m1modmmod  47989  smonoord  48002  elsetpreimafvssdm  48023  iccpartres  48055  iccpartiltu  48059  iccpartigtl  48060  iccpartgt  48064  icceuelpartlem  48072  fargshiftf1  48078  ichnreuop  48109  ichreuopeq  48110  elsprel  48112  sprsymrelfo  48134  prproropf1olem4  48143  paireqne  48148  sbcpr  48158  reupr  48159  goldbachth  48187  fmtnoprmfac1  48205  fmtnoprmfac2  48207  prmdvdsfmtnof1lem2  48225  lighneallem2  48246  lighneallem4  48250  requad2  48276  even3prm2  48372  fpprwpprb  48393  gbegt5  48414  sbgoldbwt  48430  sbgoldbm  48437  nnsum3primesgbe  48445  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  bgoldbtbndlem2  48459  bgoldbtbndlem3  48460  bgoldbtbndlem4  48461  bgoldbtbnd  48462  isubgredg  48519  grimuhgr  48540  clnbgrgrim  48587  grtriprop  48594  cycl3grtrilem  48599  cycl3grtri  48600  gpgusgralem  48709  gpgedgvtx0  48714  gpgedgvtx1  48715  gpgcubic  48732  gpg5nbgr3star  48734  gpgprismgr4cycllem3  48750  upgrwlkupwlk  48793  uspgropssxp  48797  uspgrsprfo  48801  isassintop  48863  lidldomn1  48884  2zlidl  48893  2zrngamgm  48898  2zrngmmgm  48905  rngccatidALTV  48925  rngcinvALTV  48929  rhmsubcALTVlem4  48937  funcringcsetcALTV2lem9  48951  ringccatidALTV  48959  srhmsubcALTV  48978  lmodvsmdi  49043  ply1mulgsumlem1  49050  ply1mulgsumlem2  49051  lincdifsn  49088  lincsumcl  49095  lincscmcl  49096  lincext3  49120  lindslinindsimp1  49121  lindslinindsimp2lem5  49126  snlindsntor  49135  lincresunit2  49142  lincresunit3lem2  49144  zgtp1leeq  49185  elbigo2  49216  fllog2  49232  digexp  49271  dig1  49272  nn0sumshdiglemA  49283  nn0sumshdiglemB  49284  1arymaptf1  49306  2arymaptf1  49317  rrxlinec  49400  eenglngeehlnm  49403  rrx2linest  49406  itsclc0yqsol  49428  itsclc0xyqsol  49432