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  1875  19.41v  1950  19.41  2242  nfsb4t  2503  mo4  2566  2euexv  2631  2euex  2641  raleqbidvvOLD  3305  gencl  3482  2gencl  3483  vtocl2ga  3533  vtocl2gaf  3534  vtocl3gaf  3536  vtocl3ga  3538  vtocl4g  3540  vtocl4ga  3541  rspccva  3575  2reurex  3718  2reu1  3847  rexdifi  4102  sseq0  4355  r19.2z  4452  falseral0OLD  4468  elelpwi  4564  preqsnd  4815  prproe  4861  ssuni  4888  disji2  5082  disjiun  5086  disjxiun  5095  trintss  5223  ssexg  5268  reusv2lem3  5345  propeqop  5455  otiunsndisj  5468  rexopabb  5476  pofun  5550  solin  5559  2optocl  5720  3optocl  5721  ssrelrn  5843  elrnmpt1  5909  resieq  5949  imadifssran  6109  reuop  6251  fnun  6606  fss  6678  fun  6696  fvelimab  6906  fvmptss  6953  fvn0ssdmfun  7019  fvcofneq  7038  fmptco  7074  funsndifnop  7096  fnressn  7103  fressnfv  7105  fmptsng  7114  fvtp2g  7145  fvtp3g  7146  tpres  7147  fnex  7163  funfvima3  7182  fvf1pr  7253  isores3  7281  tfisg  7796  dmfex  7847  opreuopreu  7978  releldmdifi  7989  funeldmdif  7992  el2mpocsbcl  8027  f1o2ndf1  8064  frxp  8068  fnse  8075  frxp2  8086  frxp3  8093  poseq  8100  ressuppssdif  8127  funsssuppss  8132  mpoxopxnop0  8157  reldmtpos  8176  frrlem8  8235  fpr2a  8244  smores  8284  tfrlem7  8314  tz7.48-2  8373  tz7.49  8376  oacl  8462  omcl  8463  oecl  8464  oarec  8489  oewordri  8520  oeworde  8521  oelim2  8523  oeoa  8525  oeoelem  8526  oeoe  8527  nnacl  8539  nnmcl  8540  nnecl  8541  nnmsucr  8553  naddoa  8630  brinxper  8664  2ecoptocl  8745  fsetprcnex  8799  undifixp  8872  xpf1o  9067  limensuc  9082  unfi  9095  en1eqsn  9175  ac6sfi  9184  frfi  9185  difinf  9211  imafiOLD  9216  f1dmvrnfibi  9241  f1vrnfibi  9242  suppeqfsuppbi  9282  elfiun  9333  dffi3  9334  infsupprpr  9409  xpwdomg  9490  infdiffi  9567  ttrclselem2  9635  epfrs  9640  frmin  9661  frr2  9672  rankxpsuc  9794  updjud  9846  tskwe  9862  infxpenlem  9923  fseqenlem1  9934  kmlem2  10062  nnadju  10108  cff1  10168  cflim2  10173  sornom  10187  infpssrlem4  10216  fin23lem26  10235  fin23lem30  10252  fin23lem34  10256  isf32lem11  10273  fin67  10305  isfin7-2  10306  fin1a2lem10  10319  axcc2lem  10346  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  iunfo  10449  tsk0  10674  gruina  10729  grur1a  10730  mulcanenq  10871  reclem2pr  10959  supsrlem  11022  supsr  11023  ax1rid  11072  negf1o  11567  mulgt1OLD  12000  lbreu  12092  nnindd  12165  nnaddcl  12168  nnmulcl  12169  nn0n0n1ge2b  12470  nn0indd  12589  fzind  12590  fnn0ind  12591  uzaddcl  12817  uzinfi  12841  nn01to3  12854  elpq  12888  xmulasslem2  13197  supxrunb1  13234  supxrunb2  13235  infmremnf  13259  infmrp1  13260  uzsubsubfz  13462  fzdif1  13521  elfz0ubfz0  13548  fz0fzdiffz0  13553  elfzmlbp  13555  fzofzim  13625  elfzom1elp1fzo  13648  ssfzo12bi  13677  fzoopth  13678  fzonfzoufzol  13687  elfznelfzob  13690  injresinjlem  13706  injresinj  13707  modaddmodup  13857  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  om2uzlti  13873  fsequb  13898  ssnn0fi  13908  ser1const  13981  expcllem  13995  expeq0  14015  expmordi  14090  expnngt1  14164  faclbnd  14213  hashf1rn  14275  hashgadd  14300  hashunx  14309  hashnn0n0nn  14314  hashgt0elex  14324  hashss  14332  hashfzp1  14354  hashxp  14357  hashmap  14358  hashimarni  14364  seqcoll  14387  hash2exprb  14394  hashge2el2difr  14404  elss2prb  14411  hashdifsnp1  14429  fi1uzind  14430  brfi1indALT  14433  lswlgt0cl  14492  swrdnd  14578  swrdnnn0nd  14580  swrdnd0  14581  swrd0  14582  swrdsbslen  14588  swrdspsleq  14589  pfxsuff1eqwrdeq  14622  swrdswrdlem  14627  swrdswrd  14628  wrd2ind  14646  pfxccatin12lem2a  14650  swrdccatin2  14652  pfxccatin12lem2  14654  pfxccatin12lem3  14655  pfxccatin12  14656  pfxccat3  14657  swrdccat  14658  pfxccat3a  14661  swrdccat3blem  14662  repswswrd  14707  repswrevw  14710  cshwmodn  14718  cshwsublen  14719  cshwidxmod  14726  cshwidxmodr  14727  cshf1  14733  2cshw  14736  cshweqrep  14744  cshw1  14745  2cshwcshw  14748  cshwcshid  14750  cshwcsh2id  14751  wrdlen2i  14865  2swrd2eqwrdeq  14876  wwlktovfo  14881  relexpsucnnl  14953  rtrclreclem3  14983  rtrclreclem4  14984  relexpindlem  14986  r19.29uz  15274  caubnd  15282  sqreu  15284  climshft  15499  climub  15585  climserle  15586  sumss  15647  sumss2  15649  modfsummods  15716  o1fsum  15736  binom  15753  climcndslem1  15772  climcndslem2  15773  cvgrat  15806  clim2prod  15811  prodfn0  15817  prodfrec  15818  ntrivcvgfvn0  15822  fprodn0  15902  fprodmodd  15920  fprodefsum  16018  demoivreALT  16126  ruclem8  16162  dvdsaddre2b  16234  dvdsdivcl  16243  dvdsfac  16253  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  m1exp1  16303  nn0o  16310  pwp1fsum  16318  flodddiv4  16342  smu01lem  16412  dvdslegcd  16431  gcdneg  16449  dfgcd2  16473  seq1st  16498  alginv  16502  lcmf  16560  lcmftp  16563  lcmfunsnlem2lem2  16566  lcmfunsnlem  16568  lcmfun  16572  ncoprmgcdne1b  16577  coprmproddvdslem  16589  coprmproddvds  16590  cncongr1  16594  prmdvdsexp  16642  prmndvdsfaclt  16652  ncoprmlnprm  16655  fvprmselgcd1  16973  prmgaplem6  16984  prmgaplem7  16985  prmgaplem8  16986  cshwshashlem1  17023  setsstruct2  17101  setsstruct  17103  inveq  17698  catsubcat  17763  initoeu2lem0  17937  initoeu2lem1  17938  funcestrcsetclem8  18070  funcestrcsetclem9  18071  fthestrcsetc  18073  fullestrcsetc  18074  funcsetcestrclem9  18086  fthsetcestrc  18088  fullsetcestrc  18089  lubss  18436  lubel  18437  mgmpropd  18576  issstrmgm  18578  mgmb1mgm1  18580  sgrpidmnd  18664  frmdgsum  18787  smndex1mndlem  18834  mgm2nsgrplem3  18845  dfgrp2  18892  cyccom  19132  gaass  19226  gsumwrev  19295  symgextf1lem  19349  symgextf1  19350  fvcosymgeq  19358  gsmsymgreq  19361  symgfixelsi  19364  pmtrprfv3  19383  symggen  19399  pmtrprfval  19416  gsumzres  19838  gsumpr  19884  gsumzunsnd  19885  srgmulgass  20152  srgbinom  20166  0ringnnzr  20458  rnghmsscmap  20563  rnghmsubcsetclem2  20565  rngcinv  20570  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap  20592  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  funcringcsetc  20607  srhmsubc  20613  rhmsubclem4  20621  lmodvsmmulgdi  20848  lmodfopnelem1  20849  rmodislmodlem  20880  rngqiprngimfo  21256  cnfldmulg  21358  cnfldexp  21359  ofldchr  21531  psgndiflemB  21555  assamulgscm  21857  gsumply1subr  22174  gsummoncoe1  22252  pf1ind  22299  matmulcell  22389  mat1dimscm  22419  dmatmul  22441  dmatscmcl  22447  scmataddcl  22460  scmatsubcl  22461  scmatsgrp1  22466  mavmulsolcl  22495  ma1repveval  22515  1marepvmarrepid  22519  symgmatr01lem  22597  slesolvec  22623  cramerimplem2  22628  decpmatmullem  22715  pm2mpf1  22743  mp2pm2mplem4  22753  monmat2matmon  22768  chpscmat  22786  chpscmatgsumbin  22788  fvmptnn04ifb  22795  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  cpmadugsumlemF  22820  toprntopon  22869  clsss  22998  ntrss  22999  restntr  23126  cmpsublem  23343  cmpsub  23344  2ndcrest  23398  txindislem  23577  t0kq  23762  filufint  23864  fbflim2  23921  flftg  23940  alexsubALTlem4  23994  cnextfvval  24009  ustuqtop4  24188  xmettri2  24284  mettri  24296  metss  24452  tngngp3  24600  clmvscom  25046  lmmbr  25214  caublcls  25265  lmcau  25269  ovolunlem1a  25453  nulmbl2  25493  voliunlem1  25507  iunmbl  25510  volsup  25513  dvlip  25954  dvfsumle  25982  dvfsumleOLD  25983  degltlem1  26033  ply1divex  26098  plyco  26202  dgrnznn  26208  dvnply2  26251  plydivex  26261  aannenlem2  26293  aaliou3lem2  26307  ulmcau  26360  zabsle1  27263  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  gausslemma2dlem3  27335  gausslemma2dlem4  27336  2lgslem1a1  27356  2sqnn0  27405  2sqreulem1  27413  2sqreunnlem1  27416  dchrisumlem1  27456  dchrisumlem2  27457  dchrisumlem3  27458  qabvle  27592  ostthlem2  27595  ostth2lem2  27601  nosupbnd1lem5  27680  noinfbnd1lem5  27695  nocvxminlem  27750  lesrec  27795  madebdaylemold  27894  mulsuniflem  28145  precsexlem6  28208  precsexlem7  28209  precsexlem8  28210  precsexlem9  28211  abssge0  28241  noseqind  28288  om2noseqlt  28295  om2noseqrdg  28300  n0addscl  28340  n0mulscl  28341  onsfi  28352  oldfib  28373  expscllem  28426  pw2cut2  28458  z12zsodd  28478  tgjustr  28546  axeuclidlem  29035  incistruhgr  29152  umgredgprv  29180  umgrpredgv  29213  usgredgprvALT  29268  uhgr2edg  29281  usgredg2vlem2  29299  lfuhgr1v0e  29327  subgrfun  29354  umgrres1lem  29383  upgrres1  29386  fusgrfis  29403  uhgrnbgr0nb  29427  nbgr1vtx  29431  nb3grprlem1  29453  uvtx01vtx  29470  fusgrn0degnn0  29573  vtxdginducedm1lem4  29616  finsumvtxdg2size  29624  wlkl1loop  29711  wlkres  29742  lfgrwlknloop  29761  pthdadjvtx  29801  dfpth2  29802  upgr2pthnlp  29805  upgrwlkdvdelem  29809  upgrwlkdvde  29810  uhgrwkspthlem2  29827  usgr2trlspth  29834  usgr2pth  29837  pthdlem2lem  29840  cyclnumvtx  29873  lfgrn1cycl  29878  uspgrn2crct  29881  crctcshwlkn0lem3  29885  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  iswspthsnon  29929  wlkiswwlks1  29940  wlklnwwlkln1  29941  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wlknwwlksnbij  29961  wwlksnred  29965  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnredwwlkn0  29969  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextsurj  29973  wspthsnonn0vne  29990  wspn0  29997  wwlks2onv  30026  elwwlks2  30042  elwspths2spth  30043  rusgrnumwwlk  30051  clwwlkccatlem  30064  clwlkclwwlklem2a1  30067  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlkf1lem3  30081  clwwisshclwwslem  30089  clwwisshclwwsn  30091  erclwwlktr  30097  isclwwlknx  30111  clwwlkinwwlk  30115  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  clwwlkfo  30125  clwwlkext2edg  30131  wwlksext2clwwlk  30132  wwlksubclwwlk  30133  clwwlknscsh  30137  erclwwlkntr  30146  eleclclwwlkn  30151  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwwlknon0  30168  clwwlknonel  30170  clwwlknon1  30172  clwwlknonwwlknonb  30181  clwwlknonex2lem2  30183  clwwlknun  30187  clwwlkvbij  30188  upgr3v3e3cycl  30255  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  eulerpath  30316  eucrctshift  30318  eucrct2eupth  30320  1to2vfriswmgr  30354  1to3vfriswmgr  30355  3cyclfrgrrn1  30360  4cycl2vnunb  30365  frgrwopreglem2  30388  frgrwopreglem3  30389  frgrwopreglem5ALT  30397  fusgr2wsp2nb  30409  2clwwlk2clwwlklem  30421  2clwwlk2clwwlk  30425  numclwwlk1lem2f1  30432  numclwwlk1lem2fo  30433  numclwwlk1  30436  clwwlknonclwlknonf1o  30437  dlwwlknondlwlknonf1o  30440  numclwlk1  30446  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  numclwwlk5  30463  frgrreg  30469  frgrregord013  30470  friendship  30474  nsnlplig  30556  nsnlpligALT  30557  isgrpo  30572  vcdi  30640  vcdir  30641  vcass  30642  nmosetre  30839  hlim2  31267  shscli  31392  chintcli  31406  dfch2  31482  spansncvi  31727  nmopsetretALT  31938  nmfnsetre  31952  lnopl  31989  lnfnl  32006  pjss2coi  32239  pjorthcoi  32244  pjscji  32245  pjssdif2i  32249  pjclem4a  32273  pj3lem1  32281  strlem5  32330  hstrlem5  32338  cvmdi  32399  mdslmd3i  32407  atcv1  32455  atcvat4i  32472  cdj3lem2a  32511  cdj3lem3a  32514  opreu2reuALT  32551  iuninc  32635  disji2f  32652  disjif2  32656  fmptcof2  32735  xrsmulgzz  33091  1arithufdlem3  33627  esumfzf  34226  issgon  34280  voliune  34386  volfiniune  34387  rrvsum  34611  bnj228  34891  bnj1294  34973  bnj229  35040  bnj607  35072  bnj908  35087  bnj953  35095  bnj1118  35140  bnj1174  35159  bnj1388  35189  funen1cnv  35244  rankfilimbi  35257  r1filimi  35259  trssfir1om  35267  trssfir1omregs  35292  acycgrsubgr  35352  cvmliftlem15  35492  satfsschain  35558  satfdm  35563  satf0op  35571  fmla0xp  35577  gonarlem  35588  goalrlem  35590  satffunlem1lem1  35596  satffunlem2lem1  35598  dmopab3rexdif  35599  satefvfmla0  35612  prv1n  35625  iprodefisumlem  35934  faclimlem1  35937  dfon2lem6  35980  idinside  36278  onsucconni  36631  axc11n11r  36884  bj-brrelex12ALT  37268  bj-snmoore  37318  bj-finsumval0  37490  exlimim  37547  exellim  37549  icoreclin  37562  difunieq  37579  fvineqsneq  37617  pibt2  37622  wl-spae  37726  wl-aleq  37740  fin2so  37808  matunitlindf  37819  poimirlem4  37825  poimirlem26  37847  itg2addnclem  37872  upixp  37930  welb  37937  sdclem2  37943  metf1o  37956  sstotbnd3  37977  isbndx  37983  ismtycnv  38003  heiborlem4  38015  bfplem1  38023  opidonOLD  38053  grpomndo  38076  ax12eq  39201  ax12el  39202  cvrat4  39703  nn0addcom  42717  nn0mulcom  42721  mzpexpmpt  42987  diophren  43055  rmxypos  43189  jm2.17a  43202  jm2.17b  43203  rmygeid  43206  jm2.18  43230  jm2.25  43241  jm2.15nn0  43245  jm2.16nn0  43246  pwslnm  43336  isnumbasgrplem1  43343  dgraalem  43387  onuniintrab  43468  onsupuni  43471  onsupcl3  43475  naddonnn  43637  naddwordnexlem2  43640  relexpiidm  43945  relexpmulnn  43950  relexpmulg  43951  relexp01min  43954  relexp0a  43957  relexpxpmin  43958  clsk1indlem3  44284  grucollcld  44501  dvgrat  44553  radcnvrat  44555  sspwimpcf  45160  sspwimpcfVD  45161  e2ebindALT  45169  trfr  45203  et-sqrtnegnre  47117  fsetprcnexALT  47308  eu2ndop1stv  47371  afvfv0bi  47398  afveu  47399  afvres  47418  aovmpt4g  47447  ndmaovass  47452  ndmaovdistr  47453  afv2orxorb  47474  afv2eu  47484  imarnf1pr  47528  nltle2tri  47559  fzopredsuc  47569  subsubelfzo0  47572  2ffzoeq  47573  2tceilhalfelfzo1  47578  m1modmmod  47604  smonoord  47617  elsetpreimafvssdm  47632  iccpartres  47664  iccpartiltu  47668  iccpartigtl  47669  iccpartgt  47673  icceuelpartlem  47681  fargshiftf1  47687  ichnreuop  47718  ichreuopeq  47719  elsprel  47721  sprsymrelfo  47743  prproropf1olem4  47752  paireqne  47757  sbcpr  47767  reupr  47768  goldbachth  47793  fmtnoprmfac1  47811  fmtnoprmfac2  47813  prmdvdsfmtnof1lem2  47831  lighneallem2  47852  lighneallem4  47856  requad2  47869  even3prm2  47965  fpprwpprb  47986  gbegt5  48007  sbgoldbwt  48023  sbgoldbm  48030  nnsum3primesgbe  48038  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  isubgredg  48112  grimuhgr  48133  clnbgrgrim  48180  grtriprop  48187  cycl3grtrilem  48192  cycl3grtri  48193  gpgusgralem  48302  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgcubic  48325  gpg5nbgr3star  48327  gpgprismgr4cycllem3  48343  upgrwlkupwlk  48386  uspgropssxp  48390  uspgrsprfo  48394  isassintop  48456  lidldomn1  48477  2zlidl  48486  2zrngamgm  48491  2zrngmmgm  48498  rngccatidALTV  48518  rngcinvALTV  48522  rhmsubcALTVlem4  48530  funcringcsetcALTV2lem9  48544  ringccatidALTV  48552  srhmsubcALTV  48571  lmodvsmdi  48625  ply1mulgsumlem1  48632  ply1mulgsumlem2  48633  lincdifsn  48670  lincsumcl  48677  lincscmcl  48678  lincext3  48702  lindslinindsimp1  48703  lindslinindsimp2lem5  48708  snlindsntor  48717  lincresunit2  48724  lincresunit3lem2  48726  zgtp1leeq  48767  elbigo2  48798  fllog2  48814  digexp  48853  dig1  48854  nn0sumshdiglemA  48865  nn0sumshdiglemB  48866  1arymaptf1  48888  2arymaptf1  48899  rrxlinec  48982  eenglngeehlnm  48985  rrx2linest  48988  itsclc0yqsol  49010  itsclc0xyqsol  49014