Theorem impcom 406

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  mpan9  505  bianir  1056  19.29r  1869  19.41v  1945  19.41  2223  nfsb4t  2492  mo4  2554  2euexv  2619  2euex  2629  raleqbidvvOLD  3319  gencl  3504  2gencl  3505  vtocl2ga  3557  vtocl2gaf  3558  vtocl3gaf  3560  vtocl3ga  3562  vtocl4g  3565  vtocl4ga  3566  rspccva  3605  2reurex  3752  2reu1  3887  rexdifi  4142  sseq0  4401  r19.2z  4496  ralf0  4515  falseral0  4521  elelpwi  4614  preqsnd  4861  prproe  4907  ssuni  4936  disji2  5131  invdisjrab  5135  disjiun  5136  disjxiun  5146  trintss  5285  ssexg  5324  reusv2lem3  5400  propeqop  5509  otiunsndisj  5522  rexopabb  5530  pofun  5608  solin  5615  2optocl  5773  3optocl  5774  ssrelrn  5897  elrnmpt1  5960  resieq  5996  reuop  6299  funimaexgOLD  6641  fnun  6669  fss  6739  fun  6759  fvelimab  6970  fvmptss  7016  fvn0ssdmfun  7083  fvcofneq  7102  fmptco  7138  funsndifnop  7160  fnressn  7167  fressnfv  7169  fvn0fvelrnOLD  7172  fmptsng  7177  fvtp2g  7211  fvtp3g  7212  tpres  7213  fnex  7229  funfvima3  7248  isores3  7342  tfisg  7859  dmfex  7913  opreuopreu  8039  releldmdifi  8050  funeldmdif  8053  el2mpocsbcl  8090  f1o2ndf1  8127  frxp  8131  fnse  8138  frxp2  8149  frxp3  8156  poseq  8163  ressuppssdif  8190  funsssuppss  8195  suppssOLD  8200  mpoxopxnop0  8221  reldmtpos  8240  frrlem8  8299  fpr2a  8308  wfrfunOLD  8340  wfrlem12OLD  8341  smores  8373  tfrlem7  8404  tz7.48-2  8463  tz7.49  8466  oacl  8556  omcl  8557  oecl  8558  oarec  8583  oewordri  8613  oeworde  8614  oelim2  8616  oeoa  8618  oeoelem  8619  oeoe  8620  nnacl  8632  nnmcl  8633  nnecl  8634  nnmsucr  8646  2ecoptocl  8827  fsetprcnex  8881  undifixp  8953  ssctOLD  9077  xpf1o  9164  limensuc  9179  unfi  9197  imafi  9200  en1eqsn  9299  ac6sfi  9312  frfi  9313  difinf  9342  f1dmvrnfibi  9362  f1vrnfibi  9363  suppeqfsuppbi  9404  elfiun  9455  dffi3  9456  infsupprpr  9529  xpwdomg  9610  infdiffi  9683  ttrclselem2  9751  epfrs  9756  frmin  9774  frr2  9785  rankxpsuc  9907  updjud  9959  tskwe  9975  infxpenlem  10038  fseqenlem1  10049  kmlem2  10176  nnadju  10222  cff1  10283  cflim2  10288  sornom  10302  infpssrlem4  10331  fin23lem26  10350  fin23lem30  10367  fin23lem34  10371  isf32lem11  10388  fin67  10420  isfin7-2  10421  fin1a2lem10  10434  axcc2lem  10461  axdc2lem  10473  axdc3lem2  10476  axdc3lem4  10478  axdc4lem  10480  iunfo  10564  tsk0  10788  gruina  10843  grur1a  10844  mulcanenq  10985  reclem2pr  11073  supsrlem  11136  supsr  11137  ax1rid  11186  negf1o  11676  mulgt1  12106  lbreu  12197  nnindd  12265  nnaddcl  12268  nnmulcl  12269  nn0n0n1ge2b  12573  nn0indd  12692  fzind  12693  fnn0ind  12694  uzaddcl  12921  uzinfi  12945  nn01to3  12958  elpq  12992  xmulasslem2  13296  supxrunb1  13333  supxrunb2  13334  infmremnf  13357  infmrp1  13358  uzsubsubfz  13558  elfz0ubfz0  13640  fz0fzdiffz0  13645  elfzmlbp  13647  fzofzim  13714  elfzom1elp1fzo  13734  ssfzo12bi  13762  fzoopth  13763  fzonfzoufzol  13771  elfznelfzob  13774  injresinjlem  13788  injresinj  13789  modaddmodup  13935  modfzo0difsn  13944  modsumfzodifsn  13945  addmodlteq  13947  om2uzlti  13951  fsequb  13976  ssnn0fi  13986  ser1const  14059  expcllem  14073  expeq0  14093  expmordi  14167  expnngt1  14239  faclbnd  14285  hashf1rn  14347  hashgadd  14372  hashunx  14381  hashnn0n0nn  14386  hashgt0elex  14396  hashss  14404  hashfzp1  14426  hashxp  14429  hashmap  14430  hashimarni  14436  seqcoll  14461  hash2exprb  14468  hashge2el2difr  14478  elss2prb  14484  hashdifsnp1  14493  fi1uzind  14494  brfi1indALT  14497  lswlgt0cl  14555  swrdnd  14640  swrdnnn0nd  14642  swrdnd0  14643  swrd0  14644  swrdsbslen  14650  swrdspsleq  14651  pfxsuff1eqwrdeq  14685  swrdswrdlem  14690  swrdswrd  14691  wrd2ind  14709  pfxccatin12lem2a  14713  swrdccatin2  14715  pfxccatin12lem2  14717  pfxccatin12lem3  14718  pfxccatin12  14719  pfxccat3  14720  swrdccat  14721  pfxccat3a  14724  swrdccat3blem  14725  repswswrd  14770  repswrevw  14773  cshwmodn  14781  cshwsublen  14782  cshwidxmod  14789  cshwidxmodr  14790  cshf1  14796  2cshw  14799  cshweqrep  14807  cshw1  14808  2cshwcshw  14812  cshwcshid  14814  cshwcsh2id  14815  wrdlen2i  14929  2swrd2eqwrdeq  14940  wwlktovfo  14945  relexpsucnnl  15013  rtrclreclem3  15043  rtrclreclem4  15044  relexpindlem  15046  r19.29uz  15333  caubnd  15341  sqreu  15343  climshft  15556  climub  15644  climserle  15645  sumss  15706  sumss2  15708  modfsummods  15775  o1fsum  15795  binom  15812  climcndslem1  15831  climcndslem2  15832  cvgrat  15865  clim2prod  15870  prodfn0  15876  prodfrec  15877  ntrivcvgfvn0  15881  fprodn0  15959  fprodmodd  15977  fprodefsum  16075  demoivreALT  16181  ruclem8  16217  dvdsaddre2b  16287  dvdsdivcl  16296  dvdsfac  16306  oddnn02np1  16328  oddge22np1  16329  evennn02n  16330  evennn2n  16331  m1exp1  16356  nn0o  16363  pwp1fsum  16371  flodddiv4  16393  smu01lem  16463  dvdslegcd  16482  gcdneg  16500  dfgcd2  16525  seq1st  16545  alginv  16549  lcmf  16607  lcmftp  16610  lcmfunsnlem2lem2  16613  lcmfunsnlem  16615  lcmfun  16619  ncoprmgcdne1b  16624  coprmproddvdslem  16636  coprmproddvds  16637  cncongr1  16641  prmdvdsexp  16689  prmndvdsfaclt  16700  ncoprmlnprm  16703  fvprmselgcd1  17017  prmgaplem6  17028  prmgaplem7  17029  prmgaplem8  17030  cshwshashlem1  17068  setsstruct2  17146  setsstruct  17148  inveq  17760  catsubcat  17828  initoeu2lem0  18005  initoeu2lem1  18006  funcestrcsetclem8  18141  funcestrcsetclem9  18142  fthestrcsetc  18144  fullestrcsetc  18145  funcsetcestrclem9  18157  fthsetcestrc  18159  fullsetcestrc  18160  lubss  18508  lubel  18509  mgmpropd  18614  issstrmgm  18616  mgmb1mgm1  18618  sgrpidmnd  18702  frmdgsum  18822  smndex1mndlem  18869  mgm2nsgrplem3  18880  dfgrp2  18927  cyccom  19166  gaass  19260  gsumwrev  19332  symgextf1lem  19387  symgextf1  19388  fvcosymgeq  19396  gsmsymgreq  19399  symgfixelsi  19402  pmtrprfv3  19421  symggen  19437  pmtrprfval  19454  gsumzres  19876  gsumpr  19922  gsumzunsnd  19923  srgmulgass  20169  srgbinom  20183  0ringnnzr  20474  rnghmsscmap  20575  rnghmsubcsetclem2  20577  rngcinv  20582  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap  20604  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  funcringcsetc  20619  srhmsubc  20625  rhmsubclem4  20633  lmodvsmmulgdi  20792  lmodfopnelem1  20793  rmodislmodlem  20824  rngqiprngimfo  21208  cnfldmulg  21348  cnfldexp  21349  psgndiflemB  21549  assamulgscm  21851  gsumply1subr  22176  gsummoncoe1  22252  pf1ind  22299  matmulcell  22391  mat1dimscm  22421  dmatmul  22443  dmatscmcl  22449  scmataddcl  22462  scmatsubcl  22463  scmatsgrp1  22468  mavmulsolcl  22497  ma1repveval  22517  1marepvmarrepid  22521  symgmatr01lem  22599  slesolvec  22625  cramerimplem2  22630  decpmatmullem  22717  pm2mpf1  22745  mp2pm2mplem4  22755  monmat2matmon  22770  chpscmat  22788  chpscmatgsumbin  22790  fvmptnn04ifb  22797  chfacfscmul0  22804  chfacfscmulgsum  22806  chfacfpmmul0  22808  chfacfpmmulgsum  22810  cpmadugsumlemF  22822  toprntopon  22871  clsss  23002  ntrss  23003  restntr  23130  cmpsublem  23347  cmpsub  23348  2ndcrest  23402  txindislem  23581  t0kq  23766  filufint  23868  fbflim2  23925  flftg  23944  alexsubALTlem4  23998  cnextfvval  24013  ustuqtop4  24193  xmettri2  24290  mettri  24302  metss  24461  tngngp3  24617  clmvscom  25061  lmmbr  25230  caublcls  25281  lmcau  25285  ovolunlem1a  25469  nulmbl2  25509  voliunlem1  25523  iunmbl  25526  volsup  25529  dvlip  25970  dvfsumle  25998  dvfsumleOLD  25999  degltlem1  26052  ply1divex  26117  plyco  26220  dgrnznn  26226  dvnply2  26267  plydivex  26277  aannenlem2  26309  aaliou3lem2  26323  ulmcau  26376  zabsle1  27274  gausslemma2dlem1a  27343  gausslemma2dlem2  27345  gausslemma2dlem3  27346  gausslemma2dlem4  27347  2lgslem1a1  27367  2sqnn0  27416  2sqreulem1  27424  2sqreunnlem1  27427  dchrisumlem1  27467  dchrisumlem2  27468  dchrisumlem3  27469  qabvle  27603  ostthlem2  27606  ostth2lem2  27612  nosupbnd1lem5  27691  noinfbnd1lem5  27706  nocvxminlem  27756  nocvxmin  27757  slerec  27798  madebdaylemold  27870  mulsuniflem  28099  precsexlem6  28160  precsexlem7  28161  precsexlem8  28162  precsexlem9  28163  abssge0  28189  noseqind  28215  om2noseqlt  28222  om2noseqrdg  28227  n0addscl  28262  n0mulscl  28263  tgjustr  28350  axeuclidlem  28845  incistruhgr  28964  umgredgprv  28992  umgrpredgv  29025  usgredgprvALT  29080  uhgr2edg  29093  usgredg2vlem2  29111  lfuhgr1v0e  29139  subgrfun  29166  umgrres1lem  29195  upgrres1  29198  fusgrfis  29215  uhgrnbgr0nb  29239  nbgr1vtx  29243  nb3grprlem1  29265  uvtx01vtx  29282  fusgrn0degnn0  29385  vtxdginducedm1lem4  29428  finsumvtxdg2size  29436  wlkl1loop  29524  wlkres  29556  lfgrwlknloop  29575  pthdadjvtx  29616  upgr2pthnlp  29618  upgrwlkdvdelem  29622  upgrwlkdvde  29623  uhgrwkspthlem2  29640  usgr2trlspth  29647  usgr2pth  29650  pthdlem2lem  29653  lfgrn1cycl  29688  uspgrn2crct  29691  crctcshwlkn0lem3  29695  crctcshwlkn0lem4  29696  crctcshwlkn0lem5  29697  iswspthsnon  29739  wlkiswwlks1  29750  wlklnwwlkln1  29751  wlkiswwlks2  29758  wlkiswwlksupgr2  29760  wlklnwwlkln2lem  29765  wlknwwlksnbij  29771  wwlksnred  29775  wwlksnext  29776  wwlksnredwwlkn  29778  wwlksnredwwlkn0  29779  wwlksnextfun  29781  wwlksnextinj  29782  wwlksnextsurj  29783  wspthsnonn0vne  29800  wspn0  29807  wwlks2onv  29836  elwwlks2  29849  elwspths2spth  29850  rusgrnumwwlk  29858  clwwlkccatlem  29871  clwlkclwwlklem2a1  29874  clwlkclwwlklem2fv2  29878  clwlkclwwlklem2a4  29879  clwlkclwwlklem2a  29880  clwlkclwwlklem2  29882  clwlkclwwlkf1lem3  29888  clwwisshclwwslem  29896  clwwisshclwwsn  29898  erclwwlktr  29904  isclwwlknx  29918  clwwlkinwwlk  29922  clwwlkel  29928  clwwlkf  29929  clwwlkf1  29931  clwwlkfo  29932  clwwlkext2edg  29938  wwlksext2clwwlk  29939  wwlksubclwwlk  29940  clwwlknscsh  29944  erclwwlkntr  29953  eleclclwwlkn  29958  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  clwwlknon0  29975  clwwlknonel  29977  clwwlknon1  29979  clwwlknonwwlknonb  29988  clwwlknonex2lem2  29990  clwwlknun  29994  clwwlkvbij  29995  upgr3v3e3cycl  30062  uhgr3cyclex  30064  upgr4cycl4dv4e  30067  eulerpath  30123  eucrctshift  30125  eucrct2eupth  30127  1to2vfriswmgr  30161  1to3vfriswmgr  30162  3cyclfrgrrn1  30167  4cycl2vnunb  30172  frgrwopreglem2  30195  frgrwopreglem3  30196  frgrwopreglem5ALT  30204  fusgr2wsp2nb  30216  2clwwlk2clwwlklem  30228  2clwwlk2clwwlk  30232  numclwwlk1lem2f1  30239  numclwwlk1lem2fo  30240  numclwwlk1  30243  clwwlknonclwlknonf1o  30244  dlwwlknondlwlknonf1o  30247  numclwlk1  30253  numclwlk2lem2f  30259  numclwlk2lem2f1o  30261  numclwwlk5  30270  frgrreg  30276  frgrregord013  30277  friendship  30281  nsnlplig  30363  nsnlpligALT  30364  isgrpo  30379  vcdi  30447  vcdir  30448  vcass  30449  nmosetre  30646  hlim2  31074  shscli  31199  chintcli  31213  dfch2  31289  spansncvi  31534  nmopsetretALT  31745  nmfnsetre  31759  lnopl  31796  lnfnl  31813  pjss2coi  32046  pjorthcoi  32051  pjscji  32052  pjssdif2i  32056  pjclem4a  32080  pj3lem1  32088  strlem5  32137  hstrlem5  32145  cvmdi  32206  mdslmd3i  32214  atcv1  32262  atcvat4i  32279  cdj3lem2a  32318  cdj3lem3a  32321  opreu2reuALT  32353  iuninc  32430  disji2f  32446  disjif2  32450  fmptcof2  32524  xrsmulgzz  32825  ofldchr  33128  1arithufdlem3  33361  esumfzf  33819  issgon  33873  voliune  33979  volfiniune  33980  rrvsum  34205  bnj228  34497  bnj1294  34579  bnj229  34646  bnj607  34678  bnj908  34693  bnj953  34701  bnj1118  34746  bnj1174  34765  bnj1388  34795  funen1cnv  34842  acycgrsubgr  34899  cvmliftlem15  35039  satfsschain  35105  satfdm  35110  satf0op  35118  fmla0xp  35124  gonarlem  35135  goalrlem  35137  satffunlem1lem1  35143  satffunlem2lem1  35145  dmopab3rexdif  35146  satefvfmla0  35159  prv1n  35172  iprodefisumlem  35465  faclimlem1  35468  dfon2lem6  35515  idinside  35811  onsucconni  36052  axc11n11r  36291  bj-brrelex12ALT  36677  bj-snmoore  36723  bj-finsumval0  36895  exlimim  36952  exellim  36954  icoreclin  36967  difunieq  36984  fvineqsneq  37022  pibt2  37027  wl-spae  37119  wl-aleq  37133  fin2so  37211  matunitlindf  37222  poimirlem4  37228  poimirlem26  37250  itg2addnclem  37275  upixp  37333  welb  37340  sdclem2  37346  metf1o  37359  sstotbnd3  37380  isbndx  37386  ismtycnv  37406  heiborlem4  37418  bfplem1  37426  opidonOLD  37456  grpomndo  37479  ax12eq  38543  ax12el  38544  cvrat4  39046  nn0addcom  42140  nn0mulcom  42144  mzpexpmpt  42307  diophren  42375  rmxypos  42510  jm2.17a  42523  jm2.17b  42524  rmygeid  42527  jm2.18  42551  jm2.25  42562  jm2.15nn0  42566  jm2.16nn0  42567  pwslnm  42660  isnumbasgrplem1  42667  dgraalem  42711  onuniintrab  42796  onsupuni  42799  onsupcl3  42803  naddonnn  42967  naddwordnexlem2  42970  relexpiidm  43276  relexpmulnn  43281  relexpmulg  43282  relexp01min  43285  relexp0a  43288  relexpxpmin  43289  clsk1indlem3  43615  grucollcld  43839  dvgrat  43891  radcnvrat  43893  sspwimpcf  44501  sspwimpcfVD  44502  e2ebindALT  44510  et-sqrtnegnre  46399  fsetprcnexALT  46582  eu2ndop1stv  46643  afvfv0bi  46670  afveu  46671  afvres  46690  aovmpt4g  46719  ndmaovass  46724  ndmaovdistr  46725  afv2orxorb  46746  afv2eu  46756  imarnf1pr  46800  nltle2tri  46831  fzopredsuc  46841  subsubelfzo0  46844  2ffzoeq  46845  smonoord  46848  elsetpreimafvssdm  46863  iccpartres  46895  iccpartiltu  46899  iccpartigtl  46900  iccpartgt  46904  icceuelpartlem  46912  fargshiftf1  46918  ichnreuop  46949  ichreuopeq  46950  elsprel  46952  sprsymrelfo  46974  prproropf1olem4  46983  paireqne  46988  sbcpr  46998  reupr  46999  goldbachth  47024  fmtnoprmfac1  47042  fmtnoprmfac2  47044  prmdvdsfmtnof1lem2  47062  lighneallem2  47083  lighneallem4  47087  requad2  47100  even3prm2  47196  fpprwpprb  47217  gbegt5  47238  sbgoldbwt  47254  sbgoldbm  47261  nnsum3primesgbe  47269  wtgoldbnnsum4prm  47279  bgoldbnnsum3prm  47281  bgoldbtbndlem2  47283  bgoldbtbndlem3  47284  bgoldbtbndlem4  47285  bgoldbtbnd  47286  grimuhgr  47362  gricer  47376  upgrwlkupwlk  47388  uspgropssxp  47392  uspgrsprfo  47396  isassintop  47458  lidldomn1  47479  2zlidl  47488  2zrngamgm  47493  2zrngmmgm  47500  rngccatidALTV  47520  rngcinvALTV  47524  rhmsubcALTVlem4  47532  funcringcsetcALTV2lem9  47546  ringccatidALTV  47554  srhmsubcALTV  47573  lmodvsmdi  47632  ply1mulgsumlem1  47640  ply1mulgsumlem2  47641  lincdifsn  47678  lincsumcl  47685  lincscmcl  47686  lincext3  47710  lindslinindsimp1  47711  lindslinindsimp2lem5  47716  snlindsntor  47725  lincresunit2  47732  lincresunit3lem2  47734  zgtp1leeq  47775  m1modmmod  47780  elbigo2  47811  fllog2  47827  digexp  47866  dig1  47867  nn0sumshdiglemA  47878  nn0sumshdiglemB  47879  1arymaptf1  47901  2arymaptf1  47912  rrxlinec  47995  eenglngeehlnm  47998  rrx2linest  48001  itsclc0yqsol  48023  itsclc0xyqsol  48027