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  1873  19.41v  1949  19.41  2236  nfsb4t  2507  mo4  2569  2euexv  2634  2euex  2644  raleqbidvvOLD  3343  gencl  3533  2gencl  3534  vtocl2ga  3590  vtocl2gaf  3591  vtocl3gaf  3593  vtocl3ga  3595  vtocl4g  3598  vtocl4ga  3599  rspccva  3634  2reurex  3782  2reu1  3919  rexdifi  4173  sseq0  4426  r19.2z  4518  ralf0  4537  falseral0  4539  elelpwi  4632  preqsnd  4883  prproe  4929  ssuni  4956  disji2  5150  disjiun  5154  disjxiun  5163  trintss  5302  ssexg  5341  reusv2lem3  5418  propeqop  5526  otiunsndisj  5539  rexopabb  5547  pofun  5626  solin  5634  2optocl  5795  3optocl  5796  ssrelrn  5919  elrnmpt1  5983  resieq  6020  reuop  6324  funimaexgOLD  6665  fnun  6693  fss  6763  fun  6783  fvelimab  6994  fvmptss  7041  fvn0ssdmfun  7108  fvcofneq  7127  fmptco  7163  funsndifnop  7185  fnressn  7192  fressnfv  7194  fvn0fvelrnOLD  7197  fmptsng  7202  fvtp2g  7236  fvtp3g  7237  tpres  7238  fnex  7254  funfvima3  7273  fvf1pr  7343  isores3  7371  tfisg  7891  dmfex  7945  opreuopreu  8075  releldmdifi  8086  funeldmdif  8089  el2mpocsbcl  8126  f1o2ndf1  8163  frxp  8167  fnse  8174  frxp2  8185  frxp3  8192  poseq  8199  ressuppssdif  8226  funsssuppss  8231  mpoxopxnop0  8256  reldmtpos  8275  frrlem8  8334  fpr2a  8343  wfrfunOLD  8375  wfrlem12OLD  8376  smores  8408  tfrlem7  8439  tz7.48-2  8498  tz7.49  8501  oacl  8591  omcl  8592  oecl  8593  oarec  8618  oewordri  8648  oeworde  8649  oelim2  8651  oeoa  8653  oeoelem  8654  oeoe  8655  nnacl  8667  nnmcl  8668  nnecl  8669  nnmsucr  8681  naddoa  8758  brinxper  8792  2ecoptocl  8866  fsetprcnex  8920  undifixp  8992  ssctOLD  9118  xpf1o  9205  limensuc  9220  unfi  9238  en1eqsn  9336  ac6sfi  9348  frfi  9349  difinf  9377  imafiOLD  9382  f1dmvrnfibi  9409  f1vrnfibi  9410  suppeqfsuppbi  9448  elfiun  9499  dffi3  9500  infsupprpr  9573  xpwdomg  9654  infdiffi  9727  ttrclselem2  9795  epfrs  9800  frmin  9818  frr2  9829  rankxpsuc  9951  updjud  10003  tskwe  10019  infxpenlem  10082  fseqenlem1  10093  kmlem2  10221  nnadju  10267  cff1  10327  cflim2  10332  sornom  10346  infpssrlem4  10375  fin23lem26  10394  fin23lem30  10411  fin23lem34  10415  isf32lem11  10432  fin67  10464  isfin7-2  10465  fin1a2lem10  10478  axcc2lem  10505  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  iunfo  10608  tsk0  10832  gruina  10887  grur1a  10888  mulcanenq  11029  reclem2pr  11117  supsrlem  11180  supsr  11181  ax1rid  11230  negf1o  11720  mulgt1OLD  12153  lbreu  12245  nnindd  12313  nnaddcl  12316  nnmulcl  12317  nn0n0n1ge2b  12621  nn0indd  12740  fzind  12741  fnn0ind  12742  uzaddcl  12969  uzinfi  12993  nn01to3  13006  elpq  13040  xmulasslem2  13344  supxrunb1  13381  supxrunb2  13382  infmremnf  13405  infmrp1  13406  uzsubsubfz  13606  elfz0ubfz0  13689  fz0fzdiffz0  13694  elfzmlbp  13696  fzofzim  13763  elfzom1elp1fzo  13783  ssfzo12bi  13811  fzoopth  13812  fzonfzoufzol  13820  elfznelfzob  13823  injresinjlem  13837  injresinj  13838  modaddmodup  13985  modfzo0difsn  13994  modsumfzodifsn  13995  addmodlteq  13997  om2uzlti  14001  fsequb  14026  ssnn0fi  14036  ser1const  14109  expcllem  14123  expeq0  14143  expmordi  14217  expnngt1  14290  faclbnd  14339  hashf1rn  14401  hashgadd  14426  hashunx  14435  hashnn0n0nn  14440  hashgt0elex  14450  hashss  14458  hashfzp1  14480  hashxp  14483  hashmap  14484  hashimarni  14490  seqcoll  14513  hash2exprb  14520  hashge2el2difr  14530  elss2prb  14537  hashdifsnp1  14555  fi1uzind  14556  brfi1indALT  14559  lswlgt0cl  14617  swrdnd  14702  swrdnnn0nd  14704  swrdnd0  14705  swrd0  14706  swrdsbslen  14712  swrdspsleq  14713  pfxsuff1eqwrdeq  14747  swrdswrdlem  14752  swrdswrd  14753  wrd2ind  14771  pfxccatin12lem2a  14775  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  pfxccatin12  14781  pfxccat3  14782  swrdccat  14783  pfxccat3a  14786  swrdccat3blem  14787  repswswrd  14832  repswrevw  14835  cshwmodn  14843  cshwsublen  14844  cshwidxmod  14851  cshwidxmodr  14852  cshf1  14858  2cshw  14861  cshweqrep  14869  cshw1  14870  2cshwcshw  14874  cshwcshid  14876  cshwcsh2id  14877  wrdlen2i  14991  2swrd2eqwrdeq  15002  wwlktovfo  15007  relexpsucnnl  15079  rtrclreclem3  15109  rtrclreclem4  15110  relexpindlem  15112  r19.29uz  15399  caubnd  15407  sqreu  15409  climshft  15622  climub  15710  climserle  15711  sumss  15772  sumss2  15774  modfsummods  15841  o1fsum  15861  binom  15878  climcndslem1  15897  climcndslem2  15898  cvgrat  15931  clim2prod  15936  prodfn0  15942  prodfrec  15943  ntrivcvgfvn0  15947  fprodn0  16027  fprodmodd  16045  fprodefsum  16143  demoivreALT  16249  ruclem8  16285  dvdsaddre2b  16355  dvdsdivcl  16364  dvdsfac  16374  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  m1exp1  16424  nn0o  16431  pwp1fsum  16439  flodddiv4  16461  smu01lem  16531  dvdslegcd  16550  gcdneg  16568  dfgcd2  16593  seq1st  16618  alginv  16622  lcmf  16680  lcmftp  16683  lcmfunsnlem2lem2  16686  lcmfunsnlem  16688  lcmfun  16692  ncoprmgcdne1b  16697  coprmproddvdslem  16709  coprmproddvds  16710  cncongr1  16714  prmdvdsexp  16762  prmndvdsfaclt  16772  ncoprmlnprm  16775  fvprmselgcd1  17092  prmgaplem6  17103  prmgaplem7  17104  prmgaplem8  17105  cshwshashlem1  17143  setsstruct2  17221  setsstruct  17223  inveq  17835  catsubcat  17903  initoeu2lem0  18080  initoeu2lem1  18081  funcestrcsetclem8  18216  funcestrcsetclem9  18217  fthestrcsetc  18219  fullestrcsetc  18220  funcsetcestrclem9  18232  fthsetcestrc  18234  fullsetcestrc  18235  lubss  18583  lubel  18584  mgmpropd  18689  issstrmgm  18691  mgmb1mgm1  18693  sgrpidmnd  18777  frmdgsum  18897  smndex1mndlem  18944  mgm2nsgrplem3  18955  dfgrp2  19002  cyccom  19243  gaass  19337  gsumwrev  19409  symgextf1lem  19462  symgextf1  19463  fvcosymgeq  19471  gsmsymgreq  19474  symgfixelsi  19477  pmtrprfv3  19496  symggen  19512  pmtrprfval  19529  gsumzres  19951  gsumpr  19997  gsumzunsnd  19998  srgmulgass  20244  srgbinom  20258  0ringnnzr  20551  rnghmsscmap  20652  rnghmsubcsetclem2  20654  rngcinv  20659  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap  20681  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  funcringcsetc  20696  srhmsubc  20702  rhmsubclem4  20710  lmodvsmmulgdi  20917  lmodfopnelem1  20918  rmodislmodlem  20949  rngqiprngimfo  21334  cnfldmulg  21439  cnfldexp  21440  psgndiflemB  21641  assamulgscm  21944  gsumply1subr  22256  gsummoncoe1  22333  pf1ind  22380  matmulcell  22472  mat1dimscm  22502  dmatmul  22524  dmatscmcl  22530  scmataddcl  22543  scmatsubcl  22544  scmatsgrp1  22549  mavmulsolcl  22578  ma1repveval  22598  1marepvmarrepid  22602  symgmatr01lem  22680  slesolvec  22706  cramerimplem2  22711  decpmatmullem  22798  pm2mpf1  22826  mp2pm2mplem4  22836  monmat2matmon  22851  chpscmat  22869  chpscmatgsumbin  22871  fvmptnn04ifb  22878  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  cpmadugsumlemF  22903  toprntopon  22952  clsss  23083  ntrss  23084  restntr  23211  cmpsublem  23428  cmpsub  23429  2ndcrest  23483  txindislem  23662  t0kq  23847  filufint  23949  fbflim2  24006  flftg  24025  alexsubALTlem4  24079  cnextfvval  24094  ustuqtop4  24274  xmettri2  24371  mettri  24383  metss  24542  tngngp3  24698  clmvscom  25142  lmmbr  25311  caublcls  25362  lmcau  25366  ovolunlem1a  25550  nulmbl2  25590  voliunlem1  25604  iunmbl  25607  volsup  25610  dvlip  26052  dvfsumle  26080  dvfsumleOLD  26081  degltlem1  26131  ply1divex  26196  plyco  26300  dgrnznn  26306  dvnply2  26347  plydivex  26357  aannenlem2  26389  aaliou3lem2  26403  ulmcau  26456  zabsle1  27358  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem3  27430  gausslemma2dlem4  27431  2lgslem1a1  27451  2sqnn0  27500  2sqreulem1  27508  2sqreunnlem1  27511  dchrisumlem1  27551  dchrisumlem2  27552  dchrisumlem3  27553  qabvle  27687  ostthlem2  27690  ostth2lem2  27696  nosupbnd1lem5  27775  noinfbnd1lem5  27790  nocvxminlem  27840  nocvxmin  27841  slerec  27882  madebdaylemold  27954  mulsuniflem  28193  precsexlem6  28254  precsexlem7  28255  precsexlem8  28256  precsexlem9  28257  abssge0  28287  noseqind  28316  om2noseqlt  28323  om2noseqrdg  28328  n0addscl  28365  n0mulscl  28366  expscl  28431  tgjustr  28500  axeuclidlem  28995  incistruhgr  29114  umgredgprv  29142  umgrpredgv  29175  usgredgprvALT  29230  uhgr2edg  29243  usgredg2vlem2  29261  lfuhgr1v0e  29289  subgrfun  29316  umgrres1lem  29345  upgrres1  29348  fusgrfis  29365  uhgrnbgr0nb  29389  nbgr1vtx  29393  nb3grprlem1  29415  uvtx01vtx  29432  fusgrn0degnn0  29535  vtxdginducedm1lem4  29578  finsumvtxdg2size  29586  wlkl1loop  29674  wlkres  29706  lfgrwlknloop  29725  pthdadjvtx  29766  upgr2pthnlp  29768  upgrwlkdvdelem  29772  upgrwlkdvde  29773  uhgrwkspthlem2  29790  usgr2trlspth  29797  usgr2pth  29800  pthdlem2lem  29803  lfgrn1cycl  29838  uspgrn2crct  29841  crctcshwlkn0lem3  29845  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  iswspthsnon  29889  wlkiswwlks1  29900  wlklnwwlkln1  29901  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wlknwwlksnbij  29921  wwlksnred  29925  wwlksnext  29926  wwlksnredwwlkn  29928  wwlksnredwwlkn0  29929  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextsurj  29933  wspthsnonn0vne  29950  wspn0  29957  wwlks2onv  29986  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlk  30008  clwwlkccatlem  30021  clwlkclwwlklem2a1  30024  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a4  30029  clwlkclwwlklem2a  30030  clwlkclwwlklem2  30032  clwlkclwwlkf1lem3  30038  clwwisshclwwslem  30046  clwwisshclwwsn  30048  erclwwlktr  30054  isclwwlknx  30068  clwwlkinwwlk  30072  clwwlkel  30078  clwwlkf  30079  clwwlkf1  30081  clwwlkfo  30082  clwwlkext2edg  30088  wwlksext2clwwlk  30089  wwlksubclwwlk  30090  clwwlknscsh  30094  erclwwlkntr  30103  eleclclwwlkn  30108  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwwlknon0  30125  clwwlknonel  30127  clwwlknon1  30129  clwwlknonwwlknonb  30138  clwwlknonex2lem2  30140  clwwlknun  30144  clwwlkvbij  30145  upgr3v3e3cycl  30212  uhgr3cyclex  30214  upgr4cycl4dv4e  30217  eulerpath  30273  eucrctshift  30275  eucrct2eupth  30277  1to2vfriswmgr  30311  1to3vfriswmgr  30312  3cyclfrgrrn1  30317  4cycl2vnunb  30322  frgrwopreglem2  30345  frgrwopreglem3  30346  frgrwopreglem5ALT  30354  fusgr2wsp2nb  30366  2clwwlk2clwwlklem  30378  2clwwlk2clwwlk  30382  numclwwlk1lem2f1  30389  numclwwlk1lem2fo  30390  numclwwlk1  30393  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1o  30397  numclwlk1  30403  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  numclwwlk5  30420  frgrreg  30426  frgrregord013  30427  friendship  30431  nsnlplig  30513  nsnlpligALT  30514  isgrpo  30529  vcdi  30597  vcdir  30598  vcass  30599  nmosetre  30796  hlim2  31224  shscli  31349  chintcli  31363  dfch2  31439  spansncvi  31684  nmopsetretALT  31895  nmfnsetre  31909  lnopl  31946  lnfnl  31963  pjss2coi  32196  pjorthcoi  32201  pjscji  32202  pjssdif2i  32206  pjclem4a  32230  pj3lem1  32238  strlem5  32287  hstrlem5  32295  cvmdi  32356  mdslmd3i  32364  atcv1  32412  atcvat4i  32429  cdj3lem2a  32468  cdj3lem3a  32471  opreu2reuALT  32505  iuninc  32583  disji2f  32599  disjif2  32603  fmptcof2  32675  xrsmulgzz  32992  ofldchr  33309  1arithufdlem3  33539  esumfzf  34033  issgon  34087  voliune  34193  volfiniune  34194  rrvsum  34419  bnj228  34711  bnj1294  34793  bnj229  34860  bnj607  34892  bnj908  34907  bnj953  34915  bnj1118  34960  bnj1174  34979  bnj1388  35009  funen1cnv  35064  acycgrsubgr  35126  cvmliftlem15  35266  satfsschain  35332  satfdm  35337  satf0op  35345  fmla0xp  35351  gonarlem  35362  goalrlem  35364  satffunlem1lem1  35370  satffunlem2lem1  35372  dmopab3rexdif  35373  satefvfmla0  35386  prv1n  35399  iprodefisumlem  35702  faclimlem1  35705  dfon2lem6  35752  idinside  36048  onsucconni  36403  axc11n11r  36649  bj-brrelex12ALT  37033  bj-snmoore  37079  bj-finsumval0  37251  exlimim  37308  exellim  37310  icoreclin  37323  difunieq  37340  fvineqsneq  37378  pibt2  37383  wl-spae  37475  wl-aleq  37489  fin2so  37567  matunitlindf  37578  poimirlem4  37584  poimirlem26  37606  itg2addnclem  37631  upixp  37689  welb  37696  sdclem2  37702  metf1o  37715  sstotbnd3  37736  isbndx  37742  ismtycnv  37762  heiborlem4  37774  bfplem1  37782  opidonOLD  37812  grpomndo  37835  ax12eq  38897  ax12el  38898  cvrat4  39400  nn0addcom  42426  nn0mulcom  42430  mzpexpmpt  42701  diophren  42769  rmxypos  42904  jm2.17a  42917  jm2.17b  42918  rmygeid  42921  jm2.18  42945  jm2.25  42956  jm2.15nn0  42960  jm2.16nn0  42961  pwslnm  43051  isnumbasgrplem1  43058  dgraalem  43102  onuniintrab  43187  onsupuni  43190  onsupcl3  43194  naddonnn  43357  naddwordnexlem2  43360  relexpiidm  43666  relexpmulnn  43671  relexpmulg  43672  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  clsk1indlem3  44005  grucollcld  44229  dvgrat  44281  radcnvrat  44283  sspwimpcf  44891  sspwimpcfVD  44892  e2ebindALT  44900  et-sqrtnegnre  46794  fsetprcnexALT  46977  eu2ndop1stv  47040  afvfv0bi  47067  afveu  47068  afvres  47087  aovmpt4g  47116  ndmaovass  47121  ndmaovdistr  47122  afv2orxorb  47143  afv2eu  47153  imarnf1pr  47197  nltle2tri  47228  fzopredsuc  47238  subsubelfzo0  47241  2ffzoeq  47242  smonoord  47245  elsetpreimafvssdm  47260  iccpartres  47292  iccpartiltu  47296  iccpartigtl  47297  iccpartgt  47301  icceuelpartlem  47309  fargshiftf1  47315  ichnreuop  47346  ichreuopeq  47347  elsprel  47349  sprsymrelfo  47371  prproropf1olem4  47380  paireqne  47385  sbcpr  47395  reupr  47396  goldbachth  47421  fmtnoprmfac1  47439  fmtnoprmfac2  47441  prmdvdsfmtnof1lem2  47459  lighneallem2  47480  lighneallem4  47484  requad2  47497  even3prm2  47593  fpprwpprb  47614  gbegt5  47635  sbgoldbwt  47651  sbgoldbm  47658  nnsum3primesgbe  47666  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  grimuhgr  47762  clnbgrgrim  47786  grtriprop  47792  upgrwlkupwlk  47863  uspgropssxp  47867  uspgrsprfo  47871  isassintop  47933  lidldomn1  47954  2zlidl  47963  2zrngamgm  47968  2zrngmmgm  47975  rngccatidALTV  47995  rngcinvALTV  47999  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem9  48021  ringccatidALTV  48029  srhmsubcALTV  48048  lmodvsmdi  48107  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  lincdifsn  48153  lincsumcl  48160  lincscmcl  48161  lincext3  48185  lindslinindsimp1  48186  lindslinindsimp2lem5  48191  snlindsntor  48200  lincresunit2  48207  lincresunit3lem2  48209  zgtp1leeq  48250  m1modmmod  48255  elbigo2  48286  fllog2  48302  digexp  48341  dig1  48342  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  1arymaptf1  48376  2arymaptf1  48387  rrxlinec  48470  eenglngeehlnm  48473  rrx2linest  48476  itsclc0yqsol  48498  itsclc0xyqsol  48502