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  1059  19.29r  1874  19.41v  1949  19.41  2235  nfsb4t  2504  mo4  2566  2euexv  2631  2euex  2641  raleqbidvvOLD  3335  gencl  3523  2gencl  3524  vtocl2ga  3578  vtocl2gaf  3579  vtocl3gaf  3581  vtocl3ga  3583  vtocl4g  3585  vtocl4ga  3586  rspccva  3621  2reurex  3766  2reu1  3897  rexdifi  4150  sseq0  4403  r19.2z  4495  ralf0  4514  falseral0  4516  elelpwi  4610  preqsnd  4859  prproe  4905  ssuni  4932  disji2  5127  disjiun  5131  disjxiun  5140  trintss  5278  ssexg  5323  reusv2lem3  5400  propeqop  5512  otiunsndisj  5525  rexopabb  5533  pofun  5610  solin  5619  2optocl  5781  3optocl  5782  ssrelrn  5905  elrnmpt1  5971  resieq  6008  imadifssran  6171  reuop  6313  funimaexgOLD  6654  fnun  6682  fss  6752  fun  6770  fvelimab  6981  fvmptss  7028  fvn0ssdmfun  7094  fvcofneq  7113  fmptco  7149  funsndifnop  7171  fnressn  7178  fressnfv  7180  fvn0fvelrnOLD  7183  fmptsng  7188  fvtp2g  7219  fvtp3g  7220  tpres  7221  fnex  7237  funfvima3  7256  fvf1pr  7327  isores3  7355  tfisg  7875  dmfex  7927  opreuopreu  8059  releldmdifi  8070  funeldmdif  8073  el2mpocsbcl  8110  f1o2ndf1  8147  frxp  8151  fnse  8158  frxp2  8169  frxp3  8176  poseq  8183  ressuppssdif  8210  funsssuppss  8215  mpoxopxnop0  8240  reldmtpos  8259  frrlem8  8318  fpr2a  8327  wfrfunOLD  8359  wfrlem12OLD  8360  smores  8392  tfrlem7  8423  tz7.48-2  8482  tz7.49  8485  oacl  8573  omcl  8574  oecl  8575  oarec  8600  oewordri  8630  oeworde  8631  oelim2  8633  oeoa  8635  oeoelem  8636  oeoe  8637  nnacl  8649  nnmcl  8650  nnecl  8651  nnmsucr  8663  naddoa  8740  brinxper  8774  2ecoptocl  8848  fsetprcnex  8902  undifixp  8974  ssctOLD  9092  xpf1o  9179  limensuc  9194  unfi  9211  en1eqsn  9308  ac6sfi  9320  frfi  9321  difinf  9349  imafiOLD  9354  f1dmvrnfibi  9381  f1vrnfibi  9382  suppeqfsuppbi  9419  elfiun  9470  dffi3  9471  infsupprpr  9544  xpwdomg  9625  infdiffi  9698  ttrclselem2  9766  epfrs  9771  frmin  9789  frr2  9800  rankxpsuc  9922  updjud  9974  tskwe  9990  infxpenlem  10053  fseqenlem1  10064  kmlem2  10192  nnadju  10238  cff1  10298  cflim2  10303  sornom  10317  infpssrlem4  10346  fin23lem26  10365  fin23lem30  10382  fin23lem34  10386  isf32lem11  10403  fin67  10435  isfin7-2  10436  fin1a2lem10  10449  axcc2lem  10476  axdc2lem  10488  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  iunfo  10579  tsk0  10803  gruina  10858  grur1a  10859  mulcanenq  11000  reclem2pr  11088  supsrlem  11151  supsr  11152  ax1rid  11201  negf1o  11693  mulgt1OLD  12126  lbreu  12218  nnindd  12286  nnaddcl  12289  nnmulcl  12290  nn0n0n1ge2b  12595  nn0indd  12715  fzind  12716  fnn0ind  12717  uzaddcl  12946  uzinfi  12970  nn01to3  12983  elpq  13017  xmulasslem2  13324  supxrunb1  13361  supxrunb2  13362  infmremnf  13385  infmrp1  13386  uzsubsubfz  13586  fzdif1  13645  elfz0ubfz0  13672  fz0fzdiffz0  13677  elfzmlbp  13679  fzofzim  13749  elfzom1elp1fzo  13771  ssfzo12bi  13800  fzoopth  13801  fzonfzoufzol  13809  elfznelfzob  13812  injresinjlem  13826  injresinj  13827  modaddmodup  13975  modfzo0difsn  13984  modsumfzodifsn  13985  addmodlteq  13987  om2uzlti  13991  fsequb  14016  ssnn0fi  14026  ser1const  14099  expcllem  14113  expeq0  14133  expmordi  14207  expnngt1  14280  faclbnd  14329  hashf1rn  14391  hashgadd  14416  hashunx  14425  hashnn0n0nn  14430  hashgt0elex  14440  hashss  14448  hashfzp1  14470  hashxp  14473  hashmap  14474  hashimarni  14480  seqcoll  14503  hash2exprb  14510  hashge2el2difr  14520  elss2prb  14527  hashdifsnp1  14545  fi1uzind  14546  brfi1indALT  14549  lswlgt0cl  14607  swrdnd  14692  swrdnnn0nd  14694  swrdnd0  14695  swrd0  14696  swrdsbslen  14702  swrdspsleq  14703  pfxsuff1eqwrdeq  14737  swrdswrdlem  14742  swrdswrd  14743  wrd2ind  14761  pfxccatin12lem2a  14765  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12lem3  14770  pfxccatin12  14771  pfxccat3  14772  swrdccat  14773  pfxccat3a  14776  swrdccat3blem  14777  repswswrd  14822  repswrevw  14825  cshwmodn  14833  cshwsublen  14834  cshwidxmod  14841  cshwidxmodr  14842  cshf1  14848  2cshw  14851  cshweqrep  14859  cshw1  14860  2cshwcshw  14864  cshwcshid  14866  cshwcsh2id  14867  wrdlen2i  14981  2swrd2eqwrdeq  14992  wwlktovfo  14997  relexpsucnnl  15069  rtrclreclem3  15099  rtrclreclem4  15100  relexpindlem  15102  r19.29uz  15389  caubnd  15397  sqreu  15399  climshft  15612  climub  15698  climserle  15699  sumss  15760  sumss2  15762  modfsummods  15829  o1fsum  15849  binom  15866  climcndslem1  15885  climcndslem2  15886  cvgrat  15919  clim2prod  15924  prodfn0  15930  prodfrec  15931  ntrivcvgfvn0  15935  fprodn0  16015  fprodmodd  16033  fprodefsum  16131  demoivreALT  16237  ruclem8  16273  dvdsaddre2b  16344  dvdsdivcl  16353  dvdsfac  16363  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  m1exp1  16413  nn0o  16420  pwp1fsum  16428  flodddiv4  16452  smu01lem  16522  dvdslegcd  16541  gcdneg  16559  dfgcd2  16583  seq1st  16608  alginv  16612  lcmf  16670  lcmftp  16673  lcmfunsnlem2lem2  16676  lcmfunsnlem  16678  lcmfun  16682  ncoprmgcdne1b  16687  coprmproddvdslem  16699  coprmproddvds  16700  cncongr1  16704  prmdvdsexp  16752  prmndvdsfaclt  16762  ncoprmlnprm  16765  fvprmselgcd1  17083  prmgaplem6  17094  prmgaplem7  17095  prmgaplem8  17096  cshwshashlem1  17133  setsstruct2  17211  setsstruct  17213  inveq  17818  catsubcat  17884  initoeu2lem0  18058  initoeu2lem1  18059  funcestrcsetclem8  18192  funcestrcsetclem9  18193  fthestrcsetc  18195  fullestrcsetc  18196  funcsetcestrclem9  18208  fthsetcestrc  18210  fullsetcestrc  18211  lubss  18558  lubel  18559  mgmpropd  18664  issstrmgm  18666  mgmb1mgm1  18668  sgrpidmnd  18752  frmdgsum  18875  smndex1mndlem  18922  mgm2nsgrplem3  18933  dfgrp2  18980  cyccom  19221  gaass  19315  gsumwrev  19385  symgextf1lem  19438  symgextf1  19439  fvcosymgeq  19447  gsmsymgreq  19450  symgfixelsi  19453  pmtrprfv3  19472  symggen  19488  pmtrprfval  19505  gsumzres  19927  gsumpr  19973  gsumzunsnd  19974  srgmulgass  20214  srgbinom  20228  0ringnnzr  20525  rnghmsscmap  20630  rnghmsubcsetclem2  20632  rngcinv  20637  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscmap  20659  rhmsubcsetclem2  20661  rhmsubcrngclem2  20667  funcringcsetc  20674  srhmsubc  20680  rhmsubclem4  20688  lmodvsmmulgdi  20895  lmodfopnelem1  20896  rmodislmodlem  20927  rngqiprngimfo  21311  cnfldmulg  21416  cnfldexp  21417  psgndiflemB  21618  assamulgscm  21921  gsumply1subr  22235  gsummoncoe1  22312  pf1ind  22359  matmulcell  22451  mat1dimscm  22481  dmatmul  22503  dmatscmcl  22509  scmataddcl  22522  scmatsubcl  22523  scmatsgrp1  22528  mavmulsolcl  22557  ma1repveval  22577  1marepvmarrepid  22581  symgmatr01lem  22659  slesolvec  22685  cramerimplem2  22690  decpmatmullem  22777  pm2mpf1  22805  mp2pm2mplem4  22815  monmat2matmon  22830  chpscmat  22848  chpscmatgsumbin  22850  fvmptnn04ifb  22857  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  cpmadugsumlemF  22882  toprntopon  22931  clsss  23062  ntrss  23063  restntr  23190  cmpsublem  23407  cmpsub  23408  2ndcrest  23462  txindislem  23641  t0kq  23826  filufint  23928  fbflim2  23985  flftg  24004  alexsubALTlem4  24058  cnextfvval  24073  ustuqtop4  24253  xmettri2  24350  mettri  24362  metss  24521  tngngp3  24677  clmvscom  25123  lmmbr  25292  caublcls  25343  lmcau  25347  ovolunlem1a  25531  nulmbl2  25571  voliunlem1  25585  iunmbl  25588  volsup  25591  dvlip  26032  dvfsumle  26060  dvfsumleOLD  26061  degltlem1  26111  ply1divex  26176  plyco  26280  dgrnznn  26286  dvnply2  26329  plydivex  26339  aannenlem2  26371  aaliou3lem2  26385  ulmcau  26438  zabsle1  27340  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  gausslemma2dlem4  27413  2lgslem1a1  27433  2sqnn0  27482  2sqreulem1  27490  2sqreunnlem1  27493  dchrisumlem1  27533  dchrisumlem2  27534  dchrisumlem3  27535  qabvle  27669  ostthlem2  27672  ostth2lem2  27678  nosupbnd1lem5  27757  noinfbnd1lem5  27772  nocvxminlem  27822  nocvxmin  27823  slerec  27864  madebdaylemold  27936  mulsuniflem  28175  precsexlem6  28236  precsexlem7  28237  precsexlem8  28238  precsexlem9  28239  abssge0  28269  noseqind  28298  om2noseqlt  28305  om2noseqrdg  28310  n0addscl  28347  n0mulscl  28348  expscl  28413  tgjustr  28482  axeuclidlem  28977  incistruhgr  29096  umgredgprv  29124  umgrpredgv  29157  usgredgprvALT  29212  uhgr2edg  29225  usgredg2vlem2  29243  lfuhgr1v0e  29271  subgrfun  29298  umgrres1lem  29327  upgrres1  29330  fusgrfis  29347  uhgrnbgr0nb  29371  nbgr1vtx  29375  nb3grprlem1  29397  uvtx01vtx  29414  fusgrn0degnn0  29517  vtxdginducedm1lem4  29560  finsumvtxdg2size  29568  wlkl1loop  29656  wlkres  29688  lfgrwlknloop  29707  pthdadjvtx  29748  dfpth2  29749  upgr2pthnlp  29752  upgrwlkdvdelem  29756  upgrwlkdvde  29757  uhgrwkspthlem2  29774  usgr2trlspth  29781  usgr2pth  29784  pthdlem2lem  29787  cyclnumvtx  29820  lfgrn1cycl  29825  uspgrn2crct  29828  crctcshwlkn0lem3  29832  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  iswspthsnon  29876  wlkiswwlks1  29887  wlklnwwlkln1  29888  wlkiswwlks2  29895  wlkiswwlksupgr2  29897  wlklnwwlkln2lem  29902  wlknwwlksnbij  29908  wwlksnred  29912  wwlksnext  29913  wwlksnredwwlkn  29915  wwlksnredwwlkn0  29916  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextsurj  29920  wspthsnonn0vne  29937  wspn0  29944  wwlks2onv  29973  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlk  29995  clwwlkccatlem  30008  clwlkclwwlklem2a1  30011  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  clwlkclwwlkf1lem3  30025  clwwisshclwwslem  30033  clwwisshclwwsn  30035  erclwwlktr  30041  isclwwlknx  30055  clwwlkinwwlk  30059  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  clwwlkfo  30069  clwwlkext2edg  30075  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  clwwlknscsh  30081  erclwwlkntr  30090  eleclclwwlkn  30095  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwwlknon0  30112  clwwlknonel  30114  clwwlknon1  30116  clwwlknonwwlknonb  30125  clwwlknonex2lem2  30127  clwwlknun  30131  clwwlkvbij  30132  upgr3v3e3cycl  30199  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  eulerpath  30260  eucrctshift  30262  eucrct2eupth  30264  1to2vfriswmgr  30298  1to3vfriswmgr  30299  3cyclfrgrrn1  30304  4cycl2vnunb  30309  frgrwopreglem2  30332  frgrwopreglem3  30333  frgrwopreglem5ALT  30341  fusgr2wsp2nb  30353  2clwwlk2clwwlklem  30365  2clwwlk2clwwlk  30369  numclwwlk1lem2f1  30376  numclwwlk1lem2fo  30377  numclwwlk1  30380  clwwlknonclwlknonf1o  30381  dlwwlknondlwlknonf1o  30384  numclwlk1  30390  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  numclwwlk5  30407  frgrreg  30413  frgrregord013  30414  friendship  30418  nsnlplig  30500  nsnlpligALT  30501  isgrpo  30516  vcdi  30584  vcdir  30585  vcass  30586  nmosetre  30783  hlim2  31211  shscli  31336  chintcli  31350  dfch2  31426  spansncvi  31671  nmopsetretALT  31882  nmfnsetre  31896  lnopl  31933  lnfnl  31950  pjss2coi  32183  pjorthcoi  32188  pjscji  32189  pjssdif2i  32193  pjclem4a  32217  pj3lem1  32225  strlem5  32274  hstrlem5  32282  cvmdi  32343  mdslmd3i  32351  atcv1  32399  atcvat4i  32416  cdj3lem2a  32455  cdj3lem3a  32458  opreu2reuALT  32496  iuninc  32573  disji2f  32590  disjif2  32594  fmptcof2  32667  xrsmulgzz  33011  ofldchr  33344  1arithufdlem3  33574  esumfzf  34070  issgon  34124  voliune  34230  volfiniune  34231  rrvsum  34456  bnj228  34749  bnj1294  34831  bnj229  34898  bnj607  34930  bnj908  34945  bnj953  34953  bnj1118  34998  bnj1174  35017  bnj1388  35047  funen1cnv  35102  acycgrsubgr  35163  cvmliftlem15  35303  satfsschain  35369  satfdm  35374  satf0op  35382  fmla0xp  35388  gonarlem  35399  goalrlem  35401  satffunlem1lem1  35407  satffunlem2lem1  35409  dmopab3rexdif  35410  satefvfmla0  35423  prv1n  35436  iprodefisumlem  35740  faclimlem1  35743  dfon2lem6  35789  idinside  36085  onsucconni  36438  axc11n11r  36684  bj-brrelex12ALT  37068  bj-snmoore  37114  bj-finsumval0  37286  exlimim  37343  exellim  37345  icoreclin  37358  difunieq  37375  fvineqsneq  37413  pibt2  37418  wl-spae  37522  wl-aleq  37536  fin2so  37614  matunitlindf  37625  poimirlem4  37631  poimirlem26  37653  itg2addnclem  37678  upixp  37736  welb  37743  sdclem2  37749  metf1o  37762  sstotbnd3  37783  isbndx  37789  ismtycnv  37809  heiborlem4  37821  bfplem1  37829  opidonOLD  37859  grpomndo  37882  ax12eq  38942  ax12el  38943  cvrat4  39445  nn0addcom  42480  nn0mulcom  42484  mzpexpmpt  42756  diophren  42824  rmxypos  42959  jm2.17a  42972  jm2.17b  42973  rmygeid  42976  jm2.18  43000  jm2.25  43011  jm2.15nn0  43015  jm2.16nn0  43016  pwslnm  43106  isnumbasgrplem1  43113  dgraalem  43157  onuniintrab  43238  onsupuni  43241  onsupcl3  43245  naddonnn  43408  naddwordnexlem2  43411  relexpiidm  43717  relexpmulnn  43722  relexpmulg  43723  relexp01min  43726  relexp0a  43729  relexpxpmin  43730  clsk1indlem3  44056  grucollcld  44279  dvgrat  44331  radcnvrat  44333  sspwimpcf  44940  sspwimpcfVD  44941  e2ebindALT  44949  trfr  44979  et-sqrtnegnre  46888  fsetprcnexALT  47074  eu2ndop1stv  47137  afvfv0bi  47164  afveu  47165  afvres  47184  aovmpt4g  47213  ndmaovass  47218  ndmaovdistr  47219  afv2orxorb  47240  afv2eu  47250  imarnf1pr  47294  nltle2tri  47325  fzopredsuc  47335  subsubelfzo0  47338  2ffzoeq  47339  smonoord  47358  elsetpreimafvssdm  47373  iccpartres  47405  iccpartiltu  47409  iccpartigtl  47410  iccpartgt  47414  icceuelpartlem  47422  fargshiftf1  47428  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  sprsymrelfo  47484  prproropf1olem4  47493  paireqne  47498  sbcpr  47508  reupr  47509  goldbachth  47534  fmtnoprmfac1  47552  fmtnoprmfac2  47554  prmdvdsfmtnof1lem2  47572  lighneallem2  47593  lighneallem4  47597  requad2  47610  even3prm2  47706  fpprwpprb  47727  gbegt5  47748  sbgoldbwt  47764  sbgoldbm  47771  nnsum3primesgbe  47779  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  isubgredg  47852  grimuhgr  47878  clnbgrgrim  47902  grtriprop  47908  cycl3grtrilem  47913  cycl3grtri  47914  gpgusgralem  48011  2tceilhalfelfzo1  48018  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgcubic  48035  gpg5nbgr3star  48037  upgrwlkupwlk  48056  uspgropssxp  48060  uspgrsprfo  48064  isassintop  48126  lidldomn1  48147  2zlidl  48156  2zrngamgm  48161  2zrngmmgm  48168  rngccatidALTV  48188  rngcinvALTV  48192  rhmsubcALTVlem4  48200  funcringcsetcALTV2lem9  48214  ringccatidALTV  48222  srhmsubcALTV  48241  lmodvsmdi  48295  ply1mulgsumlem1  48303  ply1mulgsumlem2  48304  lincdifsn  48341  lincsumcl  48348  lincscmcl  48349  lincext3  48373  lindslinindsimp1  48374  lindslinindsimp2lem5  48379  snlindsntor  48388  lincresunit2  48395  lincresunit3lem2  48397  zgtp1leeq  48438  m1modmmod  48442  elbigo2  48473  fllog2  48489  digexp  48528  dig1  48529  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  1arymaptf1  48563  2arymaptf1  48574  rrxlinec  48657  eenglngeehlnm  48660  rrx2linest  48663  itsclc0yqsol  48685  itsclc0xyqsol  48689