Theorem impcom 399

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  impcomdOLD  404  mpan9  499  bianir  1039  19.29r  1837  19.41v  1908  19.41  2167  nfsb4t  2460  nfsb4tALT  2531  dfeuOLD  2629  2euex  2673  gencl  3456  2gencl  3457  vtocl2ga  3495  vtocl4g  3499  rspccva  3535  2reurex  3660  2reu1  3785  sseq0  4239  r19.2z  4323  falseral0  4342  elelpwi  4435  preqsnd  4663  prproe  4710  ssuni  4734  disji2  4913  invdisjrab  4916  disjiun  4917  disjxiun  4926  trintss  5048  ssexg  5083  reusv2lem3  5154  propeqop  5253  otiunsndisj  5266  pofun  5343  solin  5350  2optocl  5496  3optocl  5497  ssrelrn  5613  elrnmpt1  5673  resieq  5709  reuop  5982  funimaexg  6273  fnun  6296  fss  6357  fun  6369  fvelimab  6566  fvmptss  6606  fvn0ssdmfun  6667  fvcofneq  6684  fmptco  6714  funsndifnop  6736  fnressn  6743  fressnfv  6745  fvn0fvelrn  6748  fmptsng  6753  fvtp2g  6788  fvtp3g  6789  tpres  6790  fnex  6806  funfvima3  6823  isores3  6911  dmfex  7456  opreuopreu  7546  el2mpocsbcl  7588  f1o2ndf1  7623  frxp  7625  fnse  7632  ressuppssdif  7654  funsssuppss  7659  suppss  7663  mpoxopxnop0  7684  reldmtpos  7703  wfrfun  7769  wfrlem12  7770  smores  7793  tfrlem7  7823  tz7.48-2  7881  tz7.49  7884  oacl  7962  omcl  7963  oecl  7964  oarec  7989  oewordri  8019  oeworde  8020  oelim2  8022  oeoa  8024  oeoelem  8025  oeoe  8026  nnacl  8038  nnmcl  8039  nnecl  8040  nnmsucr  8052  2ecoptocl  8188  undifixp  8295  ssct  8394  xpf1o  8475  limensuc  8490  ac6sfi  8557  frfi  8558  difinf  8583  f1dmvrnfibi  8603  f1vrnfibi  8604  suppeqfsuppbi  8642  elfiun  8689  dffi3  8690  infsupprpr  8763  xpwdomg  8844  infdiffi  8915  epfrs  8967  rankxpsuc  9105  updjud  9157  tskwe  9173  infxpenlem  9233  fseqenlem1  9244  kmlem2  9371  cff1  9478  cflim2  9483  sornom  9497  infpssrlem4  9526  fin23lem26  9545  fin23lem30  9562  fin23lem34  9566  isf32lem11  9583  fin67  9615  isfin7-2  9616  fin1a2lem10  9629  axcc2lem  9656  axdc2lem  9668  axdc3lem2  9671  axdc3lem4  9673  axdc4lem  9675  iunfo  9759  tsk0  9983  gruina  10038  grur1a  10039  mulcanenq  10180  reclem2pr  10268  supsrlem  10331  supsr  10332  ax1rid  10381  negf1o  10871  mulgt1  11300  fiminreOLD  11391  lbreu  11392  nnaddcl  11463  nnmulcl  11464  nn0n0n1ge2b  11775  nn0indd  11892  fzind  11893  fnn0ind  11894  uzaddcl  12118  uzinfi  12142  nn01to3  12155  elpq  12189  xmulasslem2  12491  supxrunb1  12528  supxrunb2  12529  infmremnf  12552  infmrp1  12553  uzsubsubfz  12745  elfz0ubfz0  12827  fz0fzdiffz0  12832  elfzmlbp  12834  fzofzim  12899  elfzom1elp1fzo  12919  elfzom1p1elfzo  12932  ssfzo12bi  12947  fzonfzoufzol  12955  elfznelfzob  12958  injresinjlem  12972  injresinj  12973  modaddmodup  13117  modfzo0difsn  13126  modsumfzodifsn  13127  addmodlteq  13129  om2uzlti  13133  fsequb  13158  ssnn0fi  13168  ser1const  13241  expcllem  13255  expeq0  13274  expmordi  13346  expnngt1  13417  faclbnd  13465  hashf1rn  13528  hashgadd  13551  hashunx  13560  hashnn0n0nn  13565  hashgt0elex  13575  hashss  13583  hashfzp1  13605  hashxp  13608  hashmap  13609  hashimarni  13615  seqcoll  13635  hash2exprb  13640  hashge2el2difr  13650  elss2prb  13656  hashdifsnp1  13665  fi1uzind  13666  brfi1indALT  13669  lswlgt0cl  13732  ccat1st1st  13791  swrdnd  13822  swrdnnn0nd  13824  swrdnd0  13825  swrd0  13826  swrdsbslen  13841  swrdspsleq  13842  2swrd1eqwrdeqOLD  13847  pfxsuff1eqwrdeq  13881  swrdswrdlem  13886  swrdswrd  13887  wrd2ind  13917  wrd2indOLD  13918  swrdccatfn  13923  swrdccatin1  13924  swrdccatin12lem2a  13926  swrdccatin2  13929  pfxccatin12lem2  13931  swrdccatin12lem2OLD  13932  swrdccatin12lem3  13933  pfxccatin12  13934  swrdccatin12OLD  13935  pfxccat3  13936  swrdccat3OLD  13937  swrdccat  13938  swrdccatOLD  13939  pfxccat3a  13942  swrdccat3blem  13944  repswswrd  14003  repswrevw  14006  cshwmodn  14019  cshwsublen  14020  cshwidxmod  14027  cshwidxmodr  14028  cshf1  14034  2cshw  14037  cshweqrep  14045  cshw1  14046  2cshwcshw  14049  cshwcshid  14051  cshwcsh2id  14052  wrdlen2i  14166  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  wwlktovfo  14183  relexpsucnnl  14252  rtrclreclem3  14280  rtrclreclem4  14281  relexpindlem  14283  r19.29uz  14571  caubnd  14579  sqreu  14581  climshft  14794  climub  14879  climserle  14880  sumss  14941  sumss2  14943  modfsummods  15008  o1fsum  15028  binom  15045  climcndslem1  15064  climcndslem2  15065  pwm1geoserOLD  15085  cvgrat  15099  clim2prod  15104  prodfn0  15110  prodfrec  15111  ntrivcvgfvn0  15115  fprodn0  15193  fprodmodd  15211  fprodefsum  15308  demoivreALT  15414  ruclem8  15450  dvdsaddre2b  15517  dvdsdivcl  15526  dvdsfac  15536  oddnn02np1  15557  oddge22np1  15558  evennn02n  15559  evennn2n  15560  m1exp1  15587  nn0o  15594  pwp1fsum  15602  flodddiv4  15624  smu01lem  15694  dvdslegcd  15713  gcdneg  15730  dfgcd2  15750  gcdmultiple  15756  seq1st  15771  alginv  15775  lcmf  15833  lcmftp  15836  lcmfunsnlem2lem2  15839  lcmfunsnlem  15841  lcmfun  15845  ncoprmgcdne1b  15850  coprmproddvdslem  15862  coprmproddvds  15863  cncongr1  15867  prmdvdsexp  15915  prmndvdsfaclt  15923  ncoprmlnprm  15924  fvprmselgcd1  16237  prmgaplem6  16248  prmgaplem7  16249  prmgaplem8  16250  cshwshashlem1  16285  setsstruct2  16377  setsstruct  16379  inveq  16902  catsubcat  16967  initoeu2lem0  17131  initoeu2lem1  17132  funcestrcsetclem8  17255  funcestrcsetclem9  17256  fthestrcsetc  17258  fullestrcsetc  17259  funcsetcestrclem9  17271  fthsetcestrc  17273  fullsetcestrc  17274  lubss  17589  lubel  17590  issstrmgm  17720  mgmb1mgm1  17722  frmdgsum  17868  mgm2nsgrplem3  17876  dfgrp2  17916  gaass  18198  gsumwrev  18265  symgextf1lem  18309  symgextf1  18310  fvcosymgeq  18318  gsmsymgreq  18321  symgfixelsi  18324  pmtrprfv3  18343  symggen  18359  pmtrprfval  18376  gsumzres  18783  gsumpr  18828  gsumzunsnd  18829  srgmulgass  19004  srgbinom  19018  lmodvsmmulgdi  19391  lmodfopnelem1  19392  rmodislmodlem  19423  0ringnnzr  19763  assamulgscm  19844  gsumply1subr  20105  gsummoncoe1  20175  pf1ind  20220  cnfldmulg  20279  cnfldexp  20280  psgndiflemB  20446  matmulcell  20758  mat1dimscm  20788  dmatmul  20810  dmatscmcl  20816  scmataddcl  20829  scmatsubcl  20830  scmatsgrp1  20835  mavmulsolcl  20864  ma1repveval  20884  1marepvmarrepid  20888  symgmatr01lem  20966  slesolvec  20992  cramerimplem2  20997  decpmatmullem  21083  pm2mpf1  21111  mp2pm2mplem4  21121  monmat2matmon  21136  chpscmat  21154  chpscmatgsumbin  21156  fvmptnn04ifb  21163  chfacfscmul0  21170  chfacfscmulgsum  21172  chfacfpmmul0  21174  chfacfpmmulgsum  21176  cpmadugsumlemF  21188  toprntopon  21237  clsss  21366  ntrss  21367  restntr  21494  cmpsublem  21711  cmpsub  21712  2ndcrest  21766  txindislem  21945  t0kq  22130  filufint  22232  fbflim2  22289  flftg  22308  alexsubALTlem4  22362  cnextfvval  22377  ustuqtop4  22556  xmettri2  22653  mettri  22665  metss  22821  tngngp3  22968  clmvscom  23397  lmmbr  23564  caublcls  23615  lmcau  23619  ovolunlem1a  23800  nulmbl2  23840  voliunlem1  23854  iunmbl  23857  volsup  23860  dvlip  24293  dvfsumle  24321  degltlem1  24369  ply1divex  24433  plyco  24534  dgrnznn  24540  dvnply2  24579  plydivex  24589  aannenlem2  24621  aaliou3lem2  24635  ulmcau  24686  zabsle1  25574  gausslemma2dlem1a  25643  gausslemma2dlem2  25645  gausslemma2dlem3  25646  gausslemma2dlem4  25647  2lgslem1a1  25667  2sqnn0  25716  2sqreulem1  25724  2sqreunnlem1  25727  dchrisumlem1  25767  dchrisumlem2  25768  dchrisumlem3  25769  qabvle  25903  ostthlem2  25906  ostth2lem2  25912  tgjustr  25962  axeuclidlem  26451  incistruhgr  26567  umgredgprv  26595  umgrpredgv  26628  usgredgprvALT  26680  uhgr2edg  26693  usgredg2vlem2  26711  lfuhgr1v0e  26739  subgrfun  26766  umgrres1lem  26795  upgrres1  26798  fusgrfis  26815  uhgrnbgr0nb  26839  nbgr1vtx  26843  nb3grprlem1  26865  uvtx01vtx  26882  fusgrn0degnn0  26984  vtxdginducedm1lem4  27027  finsumvtxdg2size  27035  wlkl1loop  27122  wlkres  27156  wlkresOLD  27158  lfgrwlknloop  27177  pthdadjvtx  27219  upgr2pthnlp  27221  upgrwlkdvdelem  27225  upgrwlkdvde  27226  uhgrwkspthlem2  27243  usgr2trlspth  27250  usgr2pth  27253  pthdlem2lem  27256  lfgrn1cycl  27291  uspgrn2crct  27294  crctcshwlkn0lem3  27298  crctcshwlkn0lem4  27299  crctcshwlkn0lem5  27300  iswspthsnon  27342  wlkiswwlks1  27353  wlklnwwlkln1  27354  wlkiswwlks2  27361  wlkiswwlksupgr2  27363  wlklnwwlkln2lem  27369  wlknwwlksnbij  27375  wwlksnred  27379  wwlksnredOLD  27380  wwlksnext  27381  wwlksnredwwlkn  27384  wwlksnredwwlknOLD  27385  wwlksnredwwlkn0  27386  wwlksnredwwlkn0OLD  27387  wwlksnextfun  27389  wwlksnextinj  27390  wwlksnextsurj  27391  wwlksnextfunOLD  27394  wwlksnextinjOLD  27395  wwlksnextsurOLD  27396  wspthsnonn0vne  27423  wspn0  27430  wwlks2onv  27459  elwwlks2  27472  elwspths2spth  27473  rusgrnumwwlk  27482  clwwlkccatlem  27495  clwlkclwwlklem2a1  27498  clwlkclwwlklem2fv2  27502  clwlkclwwlklem2a4  27503  clwlkclwwlklem2a  27504  clwlkclwwlklem2  27506  clwlkclwwlkf1lem3  27515  clwlkclwwlkf1lem3OLD  27516  clwwisshclwwslem  27529  clwwisshclwwsn  27531  erclwwlktr  27537  isclwwlknx  27551  clwwlkinwwlk  27555  clwwlkinwwlkOLD  27556  clwwlkel  27563  clwwlkfOLD  27564  clwwlkf1OLD  27566  clwwlkfoOLD  27567  clwwlkf  27569  clwwlkf1  27571  clwwlkfo  27572  clwwlkext2edg  27579  wwlksext2clwwlk  27580  wwlksubclwwlk  27581  wwlksubclwwlkOLD  27582  clwwlknscsh  27586  erclwwlkntr  27595  eleclclwwlkn  27600  hashecclwwlkn1  27601  umgrhashecclwwlk  27602  clwwlknon0  27621  clwwlknonel  27623  clwwlknon1  27625  clwwlknonwwlknonb  27634  clwwlknonex2lem2  27636  clwwlknun  27640  clwwlkvbij  27641  clwwlkvbijOLD  27642  upgr3v3e3cycl  27709  uhgr3cyclex  27711  upgr4cycl4dv4e  27714  eulerpath  27771  eucrctshift  27773  eucrct2eupthOLD  27776  eucrct2eupth  27777  1to2vfriswmgr  27813  1to3vfriswmgr  27814  3cyclfrgrrn1  27819  4cycl2vnunb  27824  frgrwopreglem2  27847  frgrwopreglem3  27848  frgrwopreglem5ALT  27856  fusgr2wsp2nb  27868  2clwwlk2clwwlklem  27883  2clwwlk2clwwlk  27887  2clwwlk2clwwlkOLD  27888  numclwwlk1lem2f1  27899  numclwwlk1lem2fo  27900  numclwwlk1lem2f1OLD  27904  numclwwlk1lem2foOLD  27905  numclwwlk1  27909  clwwlknonclwlknonf1o  27910  clwwlknonclwlknonf1oOLD  27911  dlwwlknondlwlknonf1o  27916  dlwwlknondlwlknonf1oOLD  27917  numclwlk1  27924  numclwlk2lem2f  27930  numclwlk2lem2f1o  27932  numclwlk2lem2fOLD  27933  numclwlk2lem2f1oOLD  27935  numclwwlk5  27945  frgrreg  27951  frgrregord013  27952  friendship  27956  nsnlplig  28035  nsnlpligALT  28036  isgrpo  28051  vcdi  28119  vcdir  28120  vcass  28121  nmosetre  28318  hlim2  28748  shscli  28875  chintcli  28889  dfch2  28965  spansncvi  29210  nmopsetretALT  29421  nmfnsetre  29435  lnopl  29472  lnfnl  29489  pjss2coi  29722  pjorthcoi  29727  pjscji  29728  pjssdif2i  29732  pjclem4a  29756  pj3lem1  29764  strlem5  29813  hstrlem5  29821  cvmdi  29882  mdslmd3i  29890  atcv1  29938  atcvat4i  29955  cdj3lem2a  29994  cdj3lem3a  29997  opreu2reuALT  30022  iuninc  30081  disji2f  30093  disjif2  30097  fmptcof2  30164  nnindd  30282  xrsmulgzz  30394  ofldchr  30563  esumfzf  30969  issgon  31024  voliune  31130  volfiniune  31131  rrvsum  31355  bnj228  31650  bnj1294  31734  bnj229  31800  bnj607  31832  bnj908  31847  bnj953  31855  bnj1118  31898  bnj1174  31917  bnj1388  31947  cvmliftlem15  32127  satf0op  32184  fmla0xp  32190  iprodefisumlem  32489  faclimlem1  32492  dfon2lem6  32550  tfisg  32573  poseq  32613  frrlem8  32648  fpr2  32658  frr2  32663  noprefixmo  32720  nosupbnd1lem5  32730  nocvxminlem  32765  nocvxmin  32766  slerec  32795  idinside  33063  onsucconni  33302  axc11n11r  33524  bj-brrelex12ALT  33865  bj-finsumval0  34027  exlimim  34062  exellim  34064  icoreclin  34077  difunieq  34094  fvineqsneq  34131  pibt2  34136  wl-spae  34201  wl-aleq  34214  fin2so  34317  matunitlindf  34328  poimirlem4  34334  poimirlem26  34356  itg2addnclem  34381  upixp  34443  welb  34450  sdclem2  34456  metf1o  34469  sstotbnd3  34493  isbndx  34499  ismtycnv  34519  heiborlem4  34531  bfplem1  34539  opidonOLD  34569  grpomndo  34592  ax12eq  35519  ax12el  35520  cvrat4  36021  mzpexpmpt  38734  diophren  38803  rmxypos  38937  jm2.17a  38950  jm2.17b  38951  rmygeid  38954  jm2.18  38978  jm2.25  38989  jm2.15nn0  38993  jm2.16nn0  38994  pwslnm  39087  isnumbasgrplem1  39094  dgraalem  39138  relexpiidm  39409  relexpmulnn  39414  relexpmulg  39415  relexp01min  39418  relexp0a  39421  relexpxpmin  39422  clsk1indlem3  39753  grucollcld  39968  dvgrat  40057  radcnvrat  40059  sspwimpcf  40670  sspwimpcfVD  40671  e2ebindALT  40679  eu2ndop1stv  42728  afvfv0bi  42755  afveu  42756  afvres  42775  aovmpt4g  42804  ndmaovass  42809  ndmaovdistr  42810  afv2orxorb  42831  afv2eu  42841  imarnf1pr  42885  nltle2tri  42917  fzopredsuc  42927  subsubelfzo0  42930  fzoopth  42931  2ffzoeq  42932  smonoord  42935  iccpartres  42948  iccpartiltu  42952  iccpartigtl  42953  iccpartgt  42957  icceuelpartlem  42965  fargshiftf1  42971  ichnreuop  43000  ichreuopeq  43001  elsprel  43003  sprsymrelfo  43025  prproropf1olem4  43034  paireqne  43039  sbcpr  43049  reupr  43050  goldbachth  43075  fmtnoprmfac1  43093  fmtnoprmfac2  43095  prmdvdsfmtnof1lem2  43113  lighneallem2  43137  lighneallem4  43141  requad2  43154  even3prm2  43250  fpprwpprb  43271  gbegt5  43292  sbgoldbwt  43308  sbgoldbm  43315  nnsum3primesgbe  43323  wtgoldbnnsum4prm  43333  bgoldbnnsum3prm  43335  bgoldbtbndlem2  43337  bgoldbtbndlem3  43338  bgoldbtbndlem4  43339  bgoldbtbnd  43340  isomuspgrlem1  43358  isomuspgrlem2d  43362  upgrwlkupwlk  43381  uspgropssxp  43385  uspgrsprfo  43389  mgmpropd  43408  isassintop  43479  lidldomn1  43554  lidlmmgm  43558  2zlidl  43567  2zrngamgm  43572  2zrngmmgm  43579  rnghmsscmap  43607  rnghmsubcsetclem2  43609  rngcinv  43614  rngccatidALTV  43622  rngcinvALTV  43626  funcrngcsetc  43631  funcrngcsetcALT  43632  rhmsscmap  43653  rhmsubcsetclem2  43655  rhmsubcrngclem2  43661  ringcinv  43665  funcringcsetc  43668  funcringcsetcALTV2lem9  43677  ringccatidALTV  43685  ringcinvALTV  43689  srhmsubc  43709  rhmsubclem4  43722  srhmsubcALTV  43727  rhmsubcALTVlem4  43740  lmodvsmdi  43794  ply1mulgsumlem1  43805  ply1mulgsumlem2  43806  lincdifsn  43844  lincsumcl  43851  lincscmcl  43852  lincext3  43876  lindslinindsimp1  43877  lindslinindsimp2lem5  43882  snlindsntor  43891  lincresunit2  43898  lincresunit3lem2  43900  zgtp1leeq  43942  m1modmmod  43947  elbigo2  43978  fllog2  43994  digexp  44033  dig1  44034  nn0sumshdiglemA  44045  nn0sumshdiglemB  44046  rrxlinec  44089  eenglngeehlnm  44092  rrx2linest  44095  itsclc0yqsol  44117  itsclc0xyqsol  44121