Theorem impcom 407

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpan9  506  bianir  1058  19.29r  1871  19.41v  1946  19.41  2232  nfsb4t  2501  mo4  2563  2euexv  2628  2euex  2638  raleqbidvvOLD  3332  gencl  3520  2gencl  3521  vtocl2ga  3577  vtocl2gaf  3578  vtocl3gaf  3580  vtocl3ga  3582  vtocl4g  3584  vtocl4ga  3585  rspccva  3620  2reurex  3768  2reu1  3905  rexdifi  4159  sseq0  4408  r19.2z  4500  ralf0  4519  falseral0  4521  elelpwi  4614  preqsnd  4863  prproe  4909  ssuni  4936  disji2  5131  disjiun  5135  disjxiun  5144  trintss  5283  ssexg  5328  reusv2lem3  5405  propeqop  5516  otiunsndisj  5529  rexopabb  5537  pofun  5614  solin  5622  2optocl  5783  3optocl  5784  ssrelrn  5907  elrnmpt1  5973  resieq  6010  reuop  6314  funimaexgOLD  6654  fnun  6682  fss  6752  fun  6770  fvelimab  6980  fvmptss  7027  fvn0ssdmfun  7093  fvcofneq  7112  fmptco  7148  funsndifnop  7170  fnressn  7177  fressnfv  7179  fvn0fvelrnOLD  7182  fmptsng  7187  fvtp2g  7218  fvtp3g  7219  tpres  7220  fnex  7236  funfvima3  7255  fvf1pr  7326  isores3  7354  tfisg  7874  dmfex  7927  opreuopreu  8057  releldmdifi  8068  funeldmdif  8071  el2mpocsbcl  8108  f1o2ndf1  8145  frxp  8149  fnse  8156  frxp2  8167  frxp3  8174  poseq  8181  ressuppssdif  8208  funsssuppss  8213  mpoxopxnop0  8238  reldmtpos  8257  frrlem8  8316  fpr2a  8325  wfrfunOLD  8357  wfrlem12OLD  8358  smores  8390  tfrlem7  8421  tz7.48-2  8480  tz7.49  8483  oacl  8571  omcl  8572  oecl  8573  oarec  8598  oewordri  8628  oeworde  8629  oelim2  8631  oeoa  8633  oeoelem  8634  oeoe  8635  nnacl  8647  nnmcl  8648  nnecl  8649  nnmsucr  8661  naddoa  8738  brinxper  8772  2ecoptocl  8846  fsetprcnex  8900  undifixp  8972  ssctOLD  9090  xpf1o  9177  limensuc  9192  unfi  9209  en1eqsn  9305  ac6sfi  9317  frfi  9318  difinf  9346  imafiOLD  9351  f1dmvrnfibi  9378  f1vrnfibi  9379  suppeqfsuppbi  9416  elfiun  9467  dffi3  9468  infsupprpr  9541  xpwdomg  9622  infdiffi  9695  ttrclselem2  9763  epfrs  9768  frmin  9786  frr2  9797  rankxpsuc  9919  updjud  9971  tskwe  9987  infxpenlem  10050  fseqenlem1  10061  kmlem2  10189  nnadju  10235  cff1  10295  cflim2  10300  sornom  10314  infpssrlem4  10343  fin23lem26  10362  fin23lem30  10379  fin23lem34  10383  isf32lem11  10400  fin67  10432  isfin7-2  10433  fin1a2lem10  10446  axcc2lem  10473  axdc2lem  10485  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  iunfo  10576  tsk0  10800  gruina  10855  grur1a  10856  mulcanenq  10997  reclem2pr  11085  supsrlem  11148  supsr  11149  ax1rid  11198  negf1o  11690  mulgt1OLD  12123  lbreu  12215  nnindd  12283  nnaddcl  12286  nnmulcl  12287  nn0n0n1ge2b  12592  nn0indd  12712  fzind  12713  fnn0ind  12714  uzaddcl  12943  uzinfi  12967  nn01to3  12980  elpq  13014  xmulasslem2  13320  supxrunb1  13357  supxrunb2  13358  infmremnf  13381  infmrp1  13382  uzsubsubfz  13582  fzdif1  13641  elfz0ubfz0  13668  fz0fzdiffz0  13673  elfzmlbp  13675  fzofzim  13745  elfzom1elp1fzo  13767  ssfzo12bi  13796  fzoopth  13797  fzonfzoufzol  13805  elfznelfzob  13808  injresinjlem  13822  injresinj  13823  modaddmodup  13971  modfzo0difsn  13980  modsumfzodifsn  13981  addmodlteq  13983  om2uzlti  13987  fsequb  14012  ssnn0fi  14022  ser1const  14095  expcllem  14109  expeq0  14129  expmordi  14203  expnngt1  14276  faclbnd  14325  hashf1rn  14387  hashgadd  14412  hashunx  14421  hashnn0n0nn  14426  hashgt0elex  14436  hashss  14444  hashfzp1  14466  hashxp  14469  hashmap  14470  hashimarni  14476  seqcoll  14499  hash2exprb  14506  hashge2el2difr  14516  elss2prb  14523  hashdifsnp1  14541  fi1uzind  14542  brfi1indALT  14545  lswlgt0cl  14603  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  swrd0  14692  swrdsbslen  14698  swrdspsleq  14699  pfxsuff1eqwrdeq  14733  swrdswrdlem  14738  swrdswrd  14739  wrd2ind  14757  pfxccatin12lem2a  14761  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccatin12  14767  pfxccat3  14768  swrdccat  14769  pfxccat3a  14772  swrdccat3blem  14773  repswswrd  14818  repswrevw  14821  cshwmodn  14829  cshwsublen  14830  cshwidxmod  14837  cshwidxmodr  14838  cshf1  14844  2cshw  14847  cshweqrep  14855  cshw1  14856  2cshwcshw  14860  cshwcshid  14862  cshwcsh2id  14863  wrdlen2i  14977  2swrd2eqwrdeq  14988  wwlktovfo  14993  relexpsucnnl  15065  rtrclreclem3  15095  rtrclreclem4  15096  relexpindlem  15098  r19.29uz  15385  caubnd  15393  sqreu  15395  climshft  15608  climub  15694  climserle  15695  sumss  15756  sumss2  15758  modfsummods  15825  o1fsum  15845  binom  15862  climcndslem1  15881  climcndslem2  15882  cvgrat  15915  clim2prod  15920  prodfn0  15926  prodfrec  15927  ntrivcvgfvn0  15931  fprodn0  16011  fprodmodd  16029  fprodefsum  16127  demoivreALT  16233  ruclem8  16269  dvdsaddre2b  16340  dvdsdivcl  16349  dvdsfac  16359  oddnn02np1  16381  oddge22np1  16382  evennn02n  16383  evennn2n  16384  m1exp1  16409  nn0o  16416  pwp1fsum  16424  flodddiv4  16448  smu01lem  16518  dvdslegcd  16537  gcdneg  16555  dfgcd2  16579  seq1st  16604  alginv  16608  lcmf  16666  lcmftp  16669  lcmfunsnlem2lem2  16672  lcmfunsnlem  16674  lcmfun  16678  ncoprmgcdne1b  16683  coprmproddvdslem  16695  coprmproddvds  16696  cncongr1  16700  prmdvdsexp  16748  prmndvdsfaclt  16758  ncoprmlnprm  16761  fvprmselgcd1  17078  prmgaplem6  17089  prmgaplem7  17090  prmgaplem8  17091  cshwshashlem1  17129  setsstruct2  17207  setsstruct  17209  inveq  17821  catsubcat  17889  initoeu2lem0  18066  initoeu2lem1  18067  funcestrcsetclem8  18202  funcestrcsetclem9  18203  fthestrcsetc  18205  fullestrcsetc  18206  funcsetcestrclem9  18218  fthsetcestrc  18220  fullsetcestrc  18221  lubss  18570  lubel  18571  mgmpropd  18676  issstrmgm  18678  mgmb1mgm1  18680  sgrpidmnd  18764  frmdgsum  18887  smndex1mndlem  18934  mgm2nsgrplem3  18945  dfgrp2  18992  cyccom  19233  gaass  19327  gsumwrev  19399  symgextf1lem  19452  symgextf1  19453  fvcosymgeq  19461  gsmsymgreq  19464  symgfixelsi  19467  pmtrprfv3  19486  symggen  19502  pmtrprfval  19519  gsumzres  19941  gsumpr  19987  gsumzunsnd  19988  srgmulgass  20234  srgbinom  20248  0ringnnzr  20541  rnghmsscmap  20646  rnghmsubcsetclem2  20648  rngcinv  20653  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap  20675  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  funcringcsetc  20690  srhmsubc  20696  rhmsubclem4  20704  lmodvsmmulgdi  20911  lmodfopnelem1  20912  rmodislmodlem  20943  rngqiprngimfo  21328  cnfldmulg  21433  cnfldexp  21434  psgndiflemB  21635  assamulgscm  21938  gsumply1subr  22250  gsummoncoe1  22327  pf1ind  22374  matmulcell  22466  mat1dimscm  22496  dmatmul  22518  dmatscmcl  22524  scmataddcl  22537  scmatsubcl  22538  scmatsgrp1  22543  mavmulsolcl  22572  ma1repveval  22592  1marepvmarrepid  22596  symgmatr01lem  22674  slesolvec  22700  cramerimplem2  22705  decpmatmullem  22792  pm2mpf1  22820  mp2pm2mplem4  22830  monmat2matmon  22845  chpscmat  22863  chpscmatgsumbin  22865  fvmptnn04ifb  22872  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  cpmadugsumlemF  22897  toprntopon  22946  clsss  23077  ntrss  23078  restntr  23205  cmpsublem  23422  cmpsub  23423  2ndcrest  23477  txindislem  23656  t0kq  23841  filufint  23943  fbflim2  24000  flftg  24019  alexsubALTlem4  24073  cnextfvval  24088  ustuqtop4  24268  xmettri2  24365  mettri  24377  metss  24536  tngngp3  24692  clmvscom  25136  lmmbr  25305  caublcls  25356  lmcau  25360  ovolunlem1a  25544  nulmbl2  25584  voliunlem1  25598  iunmbl  25601  volsup  25604  dvlip  26046  dvfsumle  26074  dvfsumleOLD  26075  degltlem1  26125  ply1divex  26190  plyco  26294  dgrnznn  26300  dvnply2  26343  plydivex  26353  aannenlem2  26385  aaliou3lem2  26399  ulmcau  26452  zabsle1  27354  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  gausslemma2dlem3  27426  gausslemma2dlem4  27427  2lgslem1a1  27447  2sqnn0  27496  2sqreulem1  27504  2sqreunnlem1  27507  dchrisumlem1  27547  dchrisumlem2  27548  dchrisumlem3  27549  qabvle  27683  ostthlem2  27686  ostth2lem2  27692  nosupbnd1lem5  27771  noinfbnd1lem5  27786  nocvxminlem  27836  nocvxmin  27837  slerec  27878  madebdaylemold  27950  mulsuniflem  28189  precsexlem6  28250  precsexlem7  28251  precsexlem8  28252  precsexlem9  28253  abssge0  28283  noseqind  28312  om2noseqlt  28319  om2noseqrdg  28324  n0addscl  28361  n0mulscl  28362  expscl  28427  tgjustr  28496  axeuclidlem  28991  incistruhgr  29110  umgredgprv  29138  umgrpredgv  29171  usgredgprvALT  29226  uhgr2edg  29239  usgredg2vlem2  29257  lfuhgr1v0e  29285  subgrfun  29312  umgrres1lem  29341  upgrres1  29344  fusgrfis  29361  uhgrnbgr0nb  29385  nbgr1vtx  29389  nb3grprlem1  29411  uvtx01vtx  29428  fusgrn0degnn0  29531  vtxdginducedm1lem4  29574  finsumvtxdg2size  29582  wlkl1loop  29670  wlkres  29702  lfgrwlknloop  29721  pthdadjvtx  29762  upgr2pthnlp  29764  upgrwlkdvdelem  29768  upgrwlkdvde  29769  uhgrwkspthlem2  29786  usgr2trlspth  29793  usgr2pth  29796  pthdlem2lem  29799  lfgrn1cycl  29834  uspgrn2crct  29837  crctcshwlkn0lem3  29841  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  iswspthsnon  29885  wlkiswwlks1  29896  wlklnwwlkln1  29897  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  wlknwwlksnbij  29917  wwlksnred  29921  wwlksnext  29922  wwlksnredwwlkn  29924  wwlksnredwwlkn0  29925  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextsurj  29929  wspthsnonn0vne  29946  wspn0  29953  wwlks2onv  29982  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlk  30004  clwwlkccatlem  30017  clwlkclwwlklem2a1  30020  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  clwlkclwwlkf1lem3  30034  clwwisshclwwslem  30042  clwwisshclwwsn  30044  erclwwlktr  30050  isclwwlknx  30064  clwwlkinwwlk  30068  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  clwwlkfo  30078  clwwlkext2edg  30084  wwlksext2clwwlk  30085  wwlksubclwwlk  30086  clwwlknscsh  30090  erclwwlkntr  30099  eleclclwwlkn  30104  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwwlknon0  30121  clwwlknonel  30123  clwwlknon1  30125  clwwlknonwwlknonb  30134  clwwlknonex2lem2  30136  clwwlknun  30140  clwwlkvbij  30141  upgr3v3e3cycl  30208  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  eulerpath  30269  eucrctshift  30271  eucrct2eupth  30273  1to2vfriswmgr  30307  1to3vfriswmgr  30308  3cyclfrgrrn1  30313  4cycl2vnunb  30318  frgrwopreglem2  30341  frgrwopreglem3  30342  frgrwopreglem5ALT  30350  fusgr2wsp2nb  30362  2clwwlk2clwwlklem  30374  2clwwlk2clwwlk  30378  numclwwlk1lem2f1  30385  numclwwlk1lem2fo  30386  numclwwlk1  30389  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1o  30393  numclwlk1  30399  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  numclwwlk5  30416  frgrreg  30422  frgrregord013  30423  friendship  30427  nsnlplig  30509  nsnlpligALT  30510  isgrpo  30525  vcdi  30593  vcdir  30594  vcass  30595  nmosetre  30792  hlim2  31220  shscli  31345  chintcli  31359  dfch2  31435  spansncvi  31680  nmopsetretALT  31891  nmfnsetre  31905  lnopl  31942  lnfnl  31959  pjss2coi  32192  pjorthcoi  32197  pjscji  32198  pjssdif2i  32202  pjclem4a  32226  pj3lem1  32234  strlem5  32283  hstrlem5  32291  cvmdi  32352  mdslmd3i  32360  atcv1  32408  atcvat4i  32425  cdj3lem2a  32464  cdj3lem3a  32467  opreu2reuALT  32504  iuninc  32580  disji2f  32596  disjif2  32600  fmptcof2  32673  xrsmulgzz  32993  ofldchr  33323  1arithufdlem3  33553  esumfzf  34049  issgon  34103  voliune  34209  volfiniune  34210  rrvsum  34435  bnj228  34727  bnj1294  34809  bnj229  34876  bnj607  34908  bnj908  34923  bnj953  34931  bnj1118  34976  bnj1174  34995  bnj1388  35025  funen1cnv  35080  acycgrsubgr  35142  cvmliftlem15  35282  satfsschain  35348  satfdm  35353  satf0op  35361  fmla0xp  35367  gonarlem  35378  goalrlem  35380  satffunlem1lem1  35386  satffunlem2lem1  35388  dmopab3rexdif  35389  satefvfmla0  35402  prv1n  35415  iprodefisumlem  35719  faclimlem1  35722  dfon2lem6  35769  idinside  36065  onsucconni  36419  axc11n11r  36665  bj-brrelex12ALT  37049  bj-snmoore  37095  bj-finsumval0  37267  exlimim  37324  exellim  37326  icoreclin  37339  difunieq  37356  fvineqsneq  37394  pibt2  37399  wl-spae  37501  wl-aleq  37515  fin2so  37593  matunitlindf  37604  poimirlem4  37610  poimirlem26  37632  itg2addnclem  37657  upixp  37715  welb  37722  sdclem2  37728  metf1o  37741  sstotbnd3  37762  isbndx  37768  ismtycnv  37788  heiborlem4  37800  bfplem1  37808  opidonOLD  37838  grpomndo  37861  ax12eq  38922  ax12el  38923  cvrat4  39425  nn0addcom  42456  nn0mulcom  42460  mzpexpmpt  42732  diophren  42800  rmxypos  42935  jm2.17a  42948  jm2.17b  42949  rmygeid  42952  jm2.18  42976  jm2.25  42987  jm2.15nn0  42991  jm2.16nn0  42992  pwslnm  43082  isnumbasgrplem1  43089  dgraalem  43133  onuniintrab  43214  onsupuni  43217  onsupcl3  43221  naddonnn  43384  naddwordnexlem2  43387  relexpiidm  43693  relexpmulnn  43698  relexpmulg  43699  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  clsk1indlem3  44032  grucollcld  44255  dvgrat  44307  radcnvrat  44309  sspwimpcf  44917  sspwimpcfVD  44918  e2ebindALT  44926  et-sqrtnegnre  46828  fsetprcnexALT  47011  eu2ndop1stv  47074  afvfv0bi  47101  afveu  47102  afvres  47121  aovmpt4g  47150  ndmaovass  47155  ndmaovdistr  47156  afv2orxorb  47177  afv2eu  47187  imarnf1pr  47231  nltle2tri  47262  fzopredsuc  47272  subsubelfzo0  47275  2ffzoeq  47276  smonoord  47295  elsetpreimafvssdm  47310  iccpartres  47342  iccpartiltu  47346  iccpartigtl  47347  iccpartgt  47351  icceuelpartlem  47359  fargshiftf1  47365  ichnreuop  47396  ichreuopeq  47397  elsprel  47399  sprsymrelfo  47421  prproropf1olem4  47430  paireqne  47435  sbcpr  47445  reupr  47446  goldbachth  47471  fmtnoprmfac1  47489  fmtnoprmfac2  47491  prmdvdsfmtnof1lem2  47509  lighneallem2  47530  lighneallem4  47534  requad2  47547  even3prm2  47643  fpprwpprb  47664  gbegt5  47685  sbgoldbwt  47701  sbgoldbm  47708  nnsum3primesgbe  47716  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  isubgredg  47789  grimuhgr  47815  clnbgrgrim  47839  grtriprop  47845  gpgusgralem  47945  2tceilhalfelfzo1  47952  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgcubic  47969  gpg5nbgr3star  47971  upgrwlkupwlk  47983  uspgropssxp  47987  uspgrsprfo  47991  isassintop  48053  lidldomn1  48074  2zlidl  48083  2zrngamgm  48088  2zrngmmgm  48095  rngccatidALTV  48115  rngcinvALTV  48119  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem9  48141  ringccatidALTV  48149  srhmsubcALTV  48168  lmodvsmdi  48223  ply1mulgsumlem1  48231  ply1mulgsumlem2  48232  lincdifsn  48269  lincsumcl  48276  lincscmcl  48277  lincext3  48301  lindslinindsimp1  48302  lindslinindsimp2lem5  48307  snlindsntor  48316  lincresunit2  48323  lincresunit3lem2  48325  zgtp1leeq  48366  m1modmmod  48370  elbigo2  48401  fllog2  48417  digexp  48456  dig1  48457  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  1arymaptf1  48491  2arymaptf1  48502  rrxlinec  48585  eenglngeehlnm  48588  rrx2linest  48591  itsclc0yqsol  48613  itsclc0xyqsol  48617