Theorem impcom 411

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpan9  514  anbiim  650  bianir  1070  19.29r  1894  19.41v  1969  19.41  2270  nfsb4t  2530  mo4  2593  2euexv  2658  2euex  2668  gencl  3495  2gencl  3496  vtocl2ga  3542  vtocl2gaf  3543  vtocl3gaf  3544  vtocl3ga  3545  vtocl4g  3546  vtocl4ga  3547  rspccva  3580  2reurex  3723  2reu1  3850  rexdifi  4103  sseq0  4357  r19.2z  4453  falseral0OLD  4469  elelpwi  4565  preqsnd  4817  prproe  4863  ssuni  4891  disji2  5084  disjiun  5088  disjxiun  5097  trintss  5226  ssexg  5279  reusv2lem3  5357  propeqop  5476  otiunsndisj  5489  rexopabb  5498  pofun  5573  solin  5582  2optocl  5743  3optocl  5744  ssrelrn  5870  elrnmpt1  5936  resieq  5976  imadifssran  6136  reuop  6280  fnun  6635  fss  6708  fun  6726  fvelimab  6939  fvmptss  6988  fvn0ssdmfun  7055  fvcofneq  7074  fmptco  7111  funsndifnop  7134  fnressn  7141  fressnfv  7143  fmptsng  7152  fvtp2g  7183  fvtp3g  7184  tpres  7185  fnex  7201  funfvima3  7220  fvf1pr  7291  isores3  7319  tfisg  7834  dmfex  7886  opreuopreu  8015  releldmdifi  8026  funeldmdif  8029  el2mpocsbcl  8064  f1o2ndf1  8101  frxp  8106  fnse  8113  frxp2  8124  frxp3  8131  poseq  8138  ressuppssdif  8165  funsssuppss  8170  mpoxopxnop0  8195  reldmtpos  8214  frrlem8  8274  fpr2a  8283  smores  8323  tfrlem7  8354  tz7.48-2  8413  tz7.49  8416  oacl  8504  omcl  8505  oecl  8506  oarec  8531  oewordri  8562  oeworde  8563  oelim2  8565  oeoa  8567  oeoelem  8568  oeoe  8569  nnacl  8581  nnmcl  8582  nnecl  8583  nnmsucr  8595  naddoa  8673  brinxper  8708  2ecoptocl  8790  fsetprcnex  8843  undifixp  8916  xpf1o  9111  limensuc  9126  unfi  9139  en1eqsn  9219  ac6sfi  9228  frfi  9229  difinf  9255  imafiOLD  9260  f1dmvrnfibi  9284  f1vrnfibi  9285  suppeqfsuppbi  9325  elfiun  9376  dffi3  9377  infsupprpr  9452  xpwdomg  9533  infdiffi  9613  ttrclselem2  9681  epfrs  9686  frmin  9707  frr2  9718  rankxpsuc  9840  updjud  9892  tskwe  9908  infxpenlem  9969  fseqenlem1  9980  kmlem2  10108  nnadju  10154  cff1  10215  cflim2  10220  sornom  10234  infpssrlem4  10263  fin23lem26  10282  fin23lem30  10299  fin23lem34  10303  isf32lem11  10320  fin67  10352  isfin7-2  10353  fin1a2lem10  10366  axcc2lem  10393  axdc2lem  10405  axdc3lem2  10408  axdc3lem4  10410  axdc4lem  10412  iunfo  10496  tsk0  10721  gruina  10776  grur1a  10777  mulcanenq  10918  reclem2pr  11006  supsrlem  11069  supsr  11070  ax1rid  11119  negf1o  11617  mulgt1OLD  12050  lbreu  12142  nnindd  12230  nnaddcl  12233  nnmulcl  12234  nn0n0n1ge2b  12550  nn0indd  12670  fzind  12671  fnn0ind  12672  uzaddcl  12905  uzinfi  12929  nn01to3  12942  elpq  12976  xmulasslem2  13285  supxrunb1  13322  supxrunb2  13323  infmremnf  13347  infmrp1  13348  uzsubsubfz  13551  fzdif1  13610  elfz0ubfz0  13637  fz0fzdiffz0  13642  elfzmlbp  13644  fzofzim  13715  elfzom1elp1fzo  13738  ssfzo12bi  13767  fzoopth  13768  fzonfzoufzol  13777  elfznelfzob  13780  injresinjlem  13796  injresinj  13797  modaddmodup  13947  modfzo0difsn  13956  modsumfzodifsn  13957  addmodlteq  13959  om2uzlti  13963  fsequb  13988  ssnn0fi  13998  ser1const  14071  expcllem  14085  expeq0  14105  expmordi  14180  expnngt1  14254  faclbnd  14303  hashf1rn  14365  hashgadd  14390  hashunx  14399  hashnn0n0nn  14404  hashgt0elex  14414  hashss  14422  hashfzp1  14444  hashxp  14447  hashmap  14448  hashimarni  14454  seqcoll  14477  hash2exprb  14484  hashge2el2difr  14494  elss2prb  14501  hashdifsnp1  14519  fi1uzind  14520  brfi1indALT  14523  lswlgt0cl  14582  swrdnd  14668  swrdnnn0nd  14670  swrdnd0  14671  swrd0  14672  swrdsbslen  14678  swrdspsleq  14679  pfxsuff1eqwrdeq  14712  swrdswrdlem  14717  swrdswrd  14718  wrd2ind  14736  pfxccatin12lem2a  14740  swrdccatin2  14742  pfxccatin12lem2  14744  pfxccatin12lem3  14745  pfxccatin12  14746  pfxccat3  14747  swrdccat  14748  pfxccat3a  14751  swrdccat3blem  14752  repswswrd  14797  repswrevw  14800  cshwmodn  14808  cshwsublen  14809  cshwidxmod  14816  cshwidxmodr  14817  cshf1  14823  2cshw  14826  cshweqrep  14834  cshw1  14835  2cshwcshw  14838  cshwcshid  14840  cshwcsh2id  14841  wrdlen2i  14955  2swrd2eqwrdeq  14966  wwlktovfo  14971  relexpsucnnl  15043  rtrclreclem3  15073  rtrclreclem4  15074  relexpindlem  15076  r19.29uz  15378  caubnd  15386  sqreu  15388  climshft  15603  climub  15689  climserle  15690  sumss  15751  sumss2  15753  modfsummods  15821  o1fsum  15841  binom  15860  climcndslem1  15879  climcndslem2  15880  cvgrat  15913  clim2prod  15918  prodfn0  15924  prodfrec  15925  ntrivcvgfvn0  15929  fprodn0  16009  fprodmodd  16027  fprodefsum  16125  demoivreALT  16233  ruclem8  16269  dvdsaddre2b  16341  dvdsdivcl  16350  dvdsfac  16360  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  m1exp1  16410  nn0o  16417  pwp1fsum  16425  flodddiv4  16449  smu01lem  16519  dvdslegcd  16538  gcdneg  16556  dfgcd2  16580  seq1st  16605  alginv  16609  lcmf  16667  lcmftp  16670  lcmfunsnlem2lem2  16673  lcmfunsnlem  16675  lcmfun  16679  ncoprmgcdne1b  16684  coprmproddvdslem  16696  coprmproddvds  16697  cncongr1  16701  prmdvdsexp  16750  prmndvdsfaclt  16760  ncoprmlnprm  16763  fvprmselgcd1  17081  prmgaplem6  17092  prmgaplem7  17093  prmgaplem8  17094  cshwshashlem1  17131  setsstruct2  17210  setsstruct  17212  inveq  17807  catsubcat  17872  initoeu2lem0  18046  initoeu2lem1  18047  funcestrcsetclem8  18179  funcestrcsetclem9  18180  fthestrcsetc  18182  fullestrcsetc  18183  funcsetcestrclem9  18195  fthsetcestrc  18197  fullsetcestrc  18198  lubss  18545  lubel  18546  mgmpropd  18685  issstrmgm  18687  mgmb1mgm1  18689  sgrpidmnd  18773  frmdgsum  18896  smndex1mndlem  18946  mgm2nsgrplem3  18957  dfgrp2  19004  cyccom  19244  gaass  19337  gsumwrev  19406  symgextf1lem  19460  symgextf1  19461  fvcosymgeq  19469  gsmsymgreq  19472  symgfixelsi  19475  pmtrprfv3  19494  symggen  19510  pmtrprfval  19527  gsumzres  19949  gsumpr  19995  gsumzunsnd  19996  srgmulgass  20263  srgbinom  20277  0ringnnzr  20571  rnghmsscmap  20676  rnghmsubcsetclem2  20678  rngcinv  20683  funcrngcsetc  20686  funcrngcsetcALT  20687  rhmsscmap  20705  rhmsubcsetclem2  20707  rhmsubcrngclem2  20713  funcringcsetc  20720  srhmsubc  20726  rhmsubclem4  20734  lmodvsmmulgdi  20961  lmodfopnelem1  20962  rmodislmodlem  20993  rngqiprngimfo  21368  cnfldmulg  21453  cnfldexp  21454  ofldchr  21625  psgndiflemB  21649  assamulgscm  21950  gsumply1subr  22292  gsummoncoe1  22368  pf1ind  22415  matmulcell  22502  mat1dimscm  22532  dmatmul  22554  dmatscmcl  22560  scmataddcl  22573  scmatsubcl  22574  scmatsgrp1  22579  mavmulsolcl  22608  ma1repveval  22628  1marepvmarrepid  22632  symgmatr01lem  22710  slesolvec  22736  cramerimplem2  22741  decpmatmullem  22828  pm2mpf1  22856  mp2pm2mplem4  22866  monmat2matmon  22881  chpscmat  22899  chpscmatgsumbin  22901  fvmptnn04ifb  22908  chfacfscmul0  22915  chfacfscmulgsum  22917  chfacfpmmul0  22919  chfacfpmmulgsum  22921  cpmadugsumlemF  22933  toprntopon  22982  clsss  23111  ntrss  23112  restntr  23239  cmpsublem  23456  cmpsub  23457  2ndcrest  23511  txindislem  23690  t0kq  23875  filufint  23977  fbflim2  24034  flftg  24053  alexsubALTlem4  24107  cnextfvval  24122  ustuqtop4  24301  xmettri2  24397  mettri  24409  metss  24565  tngngp3  24713  clmvscom  25149  lmmbr  25317  caublcls  25368  lmcau  25372  ovolunlem1a  25555  nulmbl2  25595  voliunlem1  25609  iunmbl  25612  volsup  25615  dvlip  26052  dvfsumle  26080  degltlem1  26129  ply1divex  26194  plyco  26298  dgrnznn  26304  dvnply2  26348  plydivex  26358  aannenlem2  26390  aaliou3lem2  26404  ulmcau  26455  zabsle1  27357  gausslemma2dlem1a  27426  gausslemma2dlem2  27428  gausslemma2dlem3  27429  gausslemma2dlem4  27430  2lgslem1a1  27450  2sqnn0  27499  2sqreulem1  27507  2sqreunnlem1  27510  dchrisumlem1  27550  dchrisumlem2  27551  dchrisumlem3  27552  qabvle  27686  ostthlem2  27689  ostth2lem2  27695  nosupbnd1lem5  27773  noinfbnd1lem5  27788  nocvxminlem  27844  lesrec  27889  madebdaylemold  27988  mulsuniflem  28239  precsexlem6  28302  precsexlem7  28303  precsexlem8  28304  precsexlem9  28305  abssge0  28335  noseqind  28382  om2noseqlt  28389  om2noseqrdg  28394  n0addscl  28434  n0mulscl  28435  onsfi  28446  oldfib  28467  expscllem  28520  pw2cut2  28552  z12zsodd  28572  tgjustr  28640  axeuclidlem  29160  incistruhgr  29277  umgredgprv  29305  umgrpredgv  29338  usgredgprvALT  29393  uhgr2edg  29406  usgredg2vlem2  29424  lfuhgr1v0e  29452  subgrfun  29479  umgrres1lem  29508  upgrres1  29511  fusgrfis  29528  uhgrnbgr0nb  29552  nbgr1vtx  29556  nb3grprlem1  29578  uvtx01vtx  29595  fusgrn0degnn0  29697  vtxdginducedm1lem4  29740  finsumvtxdg2size  29748  wlkl1loop  29835  wlkres  29866  lfgrwlknloop  29885  pthdadjvtx  29925  dfpth2  29926  upgr2pthnlp  29929  upgrwlkdvdelem  29933  upgrwlkdvde  29934  uhgrwkspthlem2  29951  usgr2trlspth  29958  usgr2pth  29961  pthdlem2lem  29964  cyclnumvtx  29997  lfgrn1cycl  30002  uspgrn2crct  30005  crctcshwlkn0lem3  30009  crctcshwlkn0lem4  30010  crctcshwlkn0lem5  30011  iswspthsnon  30053  wlkiswwlks1  30064  wlklnwwlkln1  30065  wlkiswwlks2  30072  wlkiswwlksupgr2  30074  wlklnwwlkln2lem  30079  wlknwwlksnbij  30085  wwlksnred  30089  wwlksnext  30090  wwlksnredwwlkn  30092  wwlksnredwwlkn0  30093  wwlksnextfun  30095  wwlksnextinj  30096  wwlksnextsurj  30097  wspthsnonn0vne  30114  wspn0  30121  wwlks2onv  30150  elwwlks2  30166  elwspths2spth  30167  rusgrnumwwlk  30175  clwwlkccatlem  30188  clwlkclwwlklem2a1  30191  clwlkclwwlklem2fv2  30195  clwlkclwwlklem2a4  30196  clwlkclwwlklem2a  30197  clwlkclwwlklem2  30199  clwlkclwwlkf1lem3  30205  clwwisshclwwslem  30213  clwwisshclwwsn  30215  erclwwlktr  30221  isclwwlknx  30235  clwwlkinwwlk  30239  clwwlkel  30245  clwwlkf  30246  clwwlkf1  30248  clwwlkfo  30249  clwwlkext2edg  30255  wwlksext2clwwlk  30256  wwlksubclwwlk  30257  clwwlknscsh  30261  erclwwlkntr  30270  eleclclwwlkn  30275  hashecclwwlkn1  30276  umgrhashecclwwlk  30277  clwwlknon0  30292  clwwlknonel  30294  clwwlknon1  30296  clwwlknonwwlknonb  30305  clwwlknonex2lem2  30307  clwwlknun  30311  clwwlkvbij  30312  upgr3v3e3cycl  30379  uhgr3cyclex  30381  upgr4cycl4dv4e  30384  eulerpath  30440  eucrctshift  30442  eucrct2eupth  30444  1to2vfriswmgr  30478  1to3vfriswmgr  30479  3cyclfrgrrn1  30484  4cycl2vnunb  30489  frgrwopreglem2  30512  frgrwopreglem3  30513  frgrwopreglem5ALT  30521  fusgr2wsp2nb  30533  2clwwlk2clwwlklem  30545  2clwwlk2clwwlk  30549  numclwwlk1lem2f1  30556  numclwwlk1lem2fo  30557  numclwwlk1  30560  clwwlknonclwlknonf1o  30561  dlwwlknondlwlknonf1o  30564  numclwlk1  30570  numclwlk2lem2f  30576  numclwlk2lem2f1o  30578  numclwwlk5  30587  frgrreg  30593  frgrregord013  30594  friendship  30598  nsnlplig  30681  nsnlpligALT  30682  isgrpo  30697  vcdi  30765  vcdir  30766  vcass  30767  nmosetre  30964  hlim2  31392  shscli  31517  chintcli  31531  dfch2  31607  spansncvi  31852  nmopsetretALT  32063  nmfnsetre  32077  lnopl  32114  lnfnl  32131  pjss2coi  32364  pjorthcoi  32369  pjscji  32370  pjssdif2i  32374  pjclem4a  32398  pj3lem1  32406  strlem5  32455  hstrlem5  32463  cvmdi  32524  mdslmd3i  32532  atcv1  32580  atcvat4i  32597  cdj3lem2a  32636  cdj3lem3a  32639  opreu2reuALT  32673  iuninc  32757  disji2f  32774  disjif2  32778  fmptcof2  32856  xrsmulgzz  33184  1arithufdlem3  33739  esumfzf  34363  issgon  34417  voliune  34523  volfiniune  34524  rrvsum  34748  bnj228  35028  bnj1294  35109  bnj229  35176  bnj607  35208  bnj908  35223  bnj953  35231  bnj1118  35276  bnj1174  35295  bnj1388  35325  funen1cnv  35379  rankfilimbi  35394  r1filimi  35396  trssfir1om  35404  trssfir1omregs  35429  acycgrsubgr  35505  cvmliftlem15  35645  satfsschain  35711  satfdm  35716  satf0op  35724  fmla0xp  35730  gonarlem  35741  goalrlem  35743  satffunlem1lem1  35749  satffunlem2lem1  35751  dmopab3rexdif  35752  satefvfmla0  35765  prv1n  35778  iprodefisumlem  36087  faclimlem1  36090  dfon2lem6  36133  idinside  36431  onsucconni  36794  axuntco  36836  ttcmin  36853  elttctr  36862  dfttc2g  36863  mh-inf3f1  36898  bj-cbvew  37111  axc11n11r  37155  bj-brrelex12ALT  37549  bj-snmoore  37600  bj-finsumval0  37774  exlimim  37833  exellim  37835  icoreclin  37848  difunieq  37865  fvineqsneq  37903  pibt2  37908  wl-spae  38021  wl-aleq  38035  fin2so  38103  matunitlindf  38114  poimirlem4  38120  poimirlem26  38142  itg2addnclem  38167  upixp  38225  welb  38232  sdclem2  38238  metf1o  38251  sstotbnd3  38272  isbndx  38278  ismtycnv  38298  heiborlem4  38310  bfplem1  38318  opidonOLD  38348  grpomndo  38371  eldisjdmqsim2  39312  ax12eq  39562  ax12el  39563  cvrat4  40064  nn0addcom  43081  nn0mulcom  43085  mzpexpmpt  43323  diophren  43387  rmxypos  43521  jm2.17a  43534  jm2.17b  43535  rmygeid  43538  jm2.18  43562  jm2.25  43573  jm2.15nn0  43577  jm2.16nn0  43578  pwslnm  43668  isnumbasgrplem1  43675  dgraalem  43719  onuniintrab  43800  onsupuni  43803  onsupcl3  43807  naddonnn  43969  naddwordnexlem2  43972  relexpiidm  44277  relexpmulnn  44282  relexpmulg  44283  relexp01min  44286  relexp0a  44289  relexpxpmin  44290  clsk1indlem3  44616  grucollcld  44833  dvgrat  44885  radcnvrat  44887  sspwimpcf  45492  sspwimpcfVD  45493  e2ebindALT  45501  trfr  45535  et-sqrtnegnre  47444  fsetprcnexALT  47653  eu2ndop1stv  47716  afvfv0bi  47743  afveu  47744  afvres  47763  aovmpt4g  47792  ndmaovass  47797  ndmaovdistr  47798  afv2orxorb  47819  afv2eu  47829  imarnf1pr  47873  nltle2tri  47904  fzopredsuc  47915  subsubelfzo0  47918  2ffzoeq  47919  2tceilhalfelfzo1  47927  m1modmmod  47955  smonoord  47968  elsetpreimafvssdm  47989  iccpartres  48021  iccpartiltu  48025  iccpartigtl  48026  iccpartgt  48030  icceuelpartlem  48038  fargshiftf1  48044  ichnreuop  48075  ichreuopeq  48076  elsprel  48078  sprsymrelfo  48100  prproropf1olem4  48109  paireqne  48114  sbcpr  48124  reupr  48125  goldbachth  48153  fmtnoprmfac1  48171  fmtnoprmfac2  48173  prmdvdsfmtnof1lem2  48191  lighneallem2  48212  lighneallem4  48216  requad2  48242  even3prm2  48338  fpprwpprb  48359  gbegt5  48380  sbgoldbwt  48396  sbgoldbm  48403  nnsum3primesgbe  48411  wtgoldbnnsum4prm  48421  bgoldbnnsum3prm  48423  bgoldbtbndlem2  48425  bgoldbtbndlem3  48426  bgoldbtbndlem4  48427  bgoldbtbnd  48428  isubgredg  48485  grimuhgr  48506  clnbgrgrim  48553  grtriprop  48560  cycl3grtrilem  48565  cycl3grtri  48566  gpgusgralem  48675  gpgedgvtx0  48680  gpgedgvtx1  48681  gpgcubic  48698  gpg5nbgr3star  48700  gpgprismgr4cycllem3  48716  upgrwlkupwlk  48759  uspgropssxp  48763  uspgrsprfo  48767  isassintop  48829  lidldomn1  48850  2zlidl  48859  2zrngamgm  48864  2zrngmmgm  48871  rngccatidALTV  48891  rngcinvALTV  48895  rhmsubcALTVlem4  48903  funcringcsetcALTV2lem9  48917  ringccatidALTV  48925  srhmsubcALTV  48944  lmodvsmdi  48998  ply1mulgsumlem1  49005  ply1mulgsumlem2  49006  lincdifsn  49043  lincsumcl  49050  lincscmcl  49051  lincext3  49075  lindslinindsimp1  49076  lindslinindsimp2lem5  49081  snlindsntor  49090  lincresunit2  49097  lincresunit3lem2  49099  zgtp1leeq  49140  elbigo2  49171  fllog2  49187  digexp  49226  dig1  49227  nn0sumshdiglemA  49238  nn0sumshdiglemB  49239  1arymaptf1  49261  2arymaptf1  49272  rrxlinec  49355  eenglngeehlnm  49358  rrx2linest  49361  itsclc0yqsol  49383  itsclc0xyqsol  49387