Theorem impcom 410

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpan9  509  bianir  1053  19.29r  1875  19.41v  1950  19.41  2237  nfsb4t  2539  nfsb4tALT  2604  mo4  2650  2euexv  2716  2euex  2726  gencl  3534  2gencl  3535  vtocl2ga  3575  vtocl4g  3579  rspccva  3622  2reurex  3750  2reu1  3881  rexdifi  4122  sseq0  4353  r19.2z  4440  falseral0  4459  elelpwi  4551  preqsnd  4789  prproe  4836  ssuni  4863  disji2  5048  invdisjrab  5052  disjiun  5053  disjxiun  5063  trintss  5189  ssexg  5227  reusv2lem3  5301  propeqop  5397  otiunsndisj  5410  rexopabb  5415  pofun  5491  solin  5498  2optocl  5646  3optocl  5647  ssrelrn  5763  elrnmpt1  5830  resieq  5864  reuop  6144  funimaexg  6440  fnun  6463  fss  6527  fun  6540  fvelimab  6737  fvmptss  6780  fvn0ssdmfun  6842  fvcofneq  6859  fmptco  6891  funsndifnop  6913  fnressn  6920  fressnfv  6922  fvn0fvelrn  6925  fmptsng  6930  fvtp2g  6961  fvtp3g  6962  tpres  6963  fnex  6980  funfvima3  6998  isores3  7088  dmfex  7641  opreuopreu  7734  releldmdifi  7744  funeldmdif  7747  el2mpocsbcl  7780  f1o2ndf1  7818  frxp  7820  fnse  7827  ressuppssdif  7851  funsssuppss  7856  suppss  7860  mpoxopxnop0  7881  reldmtpos  7900  wfrfun  7965  wfrlem12  7966  smores  7989  tfrlem7  8019  tz7.48-2  8078  tz7.49  8081  oacl  8160  omcl  8161  oecl  8162  oarec  8188  oewordri  8218  oeworde  8219  oelim2  8221  oeoa  8223  oeoelem  8224  oeoe  8225  nnacl  8237  nnmcl  8238  nnecl  8239  nnmsucr  8251  2ecoptocl  8388  undifixp  8498  ssct  8598  xpf1o  8679  limensuc  8694  ac6sfi  8762  frfi  8763  difinf  8788  f1dmvrnfibi  8808  f1vrnfibi  8809  suppeqfsuppbi  8847  elfiun  8894  dffi3  8895  infsupprpr  8968  xpwdomg  9049  infdiffi  9121  epfrs  9173  rankxpsuc  9311  updjud  9363  tskwe  9379  infxpenlem  9439  fseqenlem1  9450  kmlem2  9577  cff1  9680  cflim2  9685  sornom  9699  infpssrlem4  9728  fin23lem26  9747  fin23lem30  9764  fin23lem34  9768  isf32lem11  9785  fin67  9817  isfin7-2  9818  fin1a2lem10  9831  axcc2lem  9858  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  iunfo  9961  tsk0  10185  gruina  10240  grur1a  10241  mulcanenq  10382  reclem2pr  10470  supsrlem  10533  supsr  10534  ax1rid  10583  negf1o  11070  mulgt1  11499  fiminreOLD  11590  lbreu  11591  nnindd  11658  nnaddcl  11661  nnmulcl  11662  nn0n0n1ge2b  11964  nn0indd  12080  fzind  12081  fnn0ind  12082  uzaddcl  12305  uzinfi  12329  nn01to3  12342  elpq  12375  xmulasslem2  12676  supxrunb1  12713  supxrunb2  12714  infmremnf  12737  infmrp1  12738  uzsubsubfz  12930  elfz0ubfz0  13012  fz0fzdiffz0  13017  elfzmlbp  13019  fzofzim  13085  elfzom1elp1fzo  13105  ssfzo12bi  13133  fzonfzoufzol  13141  elfznelfzob  13144  injresinjlem  13158  injresinj  13159  modaddmodup  13303  modfzo0difsn  13312  modsumfzodifsn  13313  addmodlteq  13315  om2uzlti  13319  fsequb  13344  ssnn0fi  13354  ser1const  13427  expcllem  13441  expeq0  13460  expmordi  13532  expnngt1  13603  faclbnd  13651  hashf1rn  13714  hashgadd  13739  hashunx  13748  hashnn0n0nn  13753  hashgt0elex  13763  hashss  13771  hashfzp1  13793  hashxp  13796  hashmap  13797  hashimarni  13803  seqcoll  13823  hash2exprb  13830  hashge2el2difr  13840  elss2prb  13846  hashdifsnp1  13855  fi1uzind  13856  brfi1indALT  13859  lswlgt0cl  13921  swrdnd  14016  swrdnnn0nd  14018  swrdnd0  14019  swrd0  14020  swrdsbslen  14026  swrdspsleq  14027  pfxsuff1eqwrdeq  14061  swrdswrdlem  14066  swrdswrd  14067  wrd2ind  14085  pfxccatin12lem2a  14089  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  pfxccatin12  14095  pfxccat3  14096  swrdccat  14097  pfxccat3a  14100  swrdccat3blem  14101  repswswrd  14146  repswrevw  14149  cshwmodn  14157  cshwsublen  14158  cshwidxmod  14165  cshwidxmodr  14166  cshf1  14172  2cshw  14175  cshweqrep  14183  cshw1  14184  2cshwcshw  14187  cshwcshid  14189  cshwcsh2id  14190  wrdlen2i  14304  2swrd2eqwrdeq  14315  wwlktovfo  14322  relexpsucnnl  14391  rtrclreclem3  14419  rtrclreclem4  14420  relexpindlem  14422  r19.29uz  14710  caubnd  14718  sqreu  14720  climshft  14933  climub  15018  climserle  15019  sumss  15081  sumss2  15083  modfsummods  15148  o1fsum  15168  binom  15185  climcndslem1  15204  climcndslem2  15205  pwm1geoserOLD  15225  cvgrat  15239  clim2prod  15244  prodfn0  15250  prodfrec  15251  ntrivcvgfvn0  15255  fprodn0  15333  fprodmodd  15351  fprodefsum  15448  demoivreALT  15554  ruclem8  15590  dvdsaddre2b  15657  dvdsdivcl  15666  dvdsfac  15676  oddnn02np1  15697  oddge22np1  15698  evennn02n  15699  evennn2n  15700  m1exp1  15727  nn0o  15734  pwp1fsum  15742  flodddiv4  15764  smu01lem  15834  dvdslegcd  15853  gcdneg  15870  dfgcd2  15894  gcdmultipleOLD  15900  seq1st  15915  alginv  15919  lcmf  15977  lcmftp  15980  lcmfunsnlem2lem2  15983  lcmfunsnlem  15985  lcmfun  15989  ncoprmgcdne1b  15994  coprmproddvdslem  16006  coprmproddvds  16007  cncongr1  16011  prmdvdsexp  16059  prmndvdsfaclt  16067  ncoprmlnprm  16068  fvprmselgcd1  16381  prmgaplem6  16392  prmgaplem7  16393  prmgaplem8  16394  cshwshashlem1  16429  setsstruct2  16521  setsstruct  16523  inveq  17044  catsubcat  17109  initoeu2lem0  17273  initoeu2lem1  17274  funcestrcsetclem8  17397  funcestrcsetclem9  17398  fthestrcsetc  17400  fullestrcsetc  17401  funcsetcestrclem9  17413  fthsetcestrc  17415  fullsetcestrc  17416  lubss  17731  lubel  17732  issstrmgm  17863  mgmb1mgm1  17865  sgrpidmnd  17916  frmdgsum  18027  smndex1mndlem  18074  mgm2nsgrplem3  18085  dfgrp2  18128  cyccom  18346  gaass  18427  gsumwrev  18494  symgextf1lem  18548  symgextf1  18549  fvcosymgeq  18557  gsmsymgreq  18560  symgfixelsi  18563  pmtrprfv3  18582  symggen  18598  pmtrprfval  18615  gsumzres  19029  gsumpr  19075  gsumzunsnd  19076  srgmulgass  19281  srgbinom  19295  lmodvsmmulgdi  19669  lmodfopnelem1  19670  rmodislmodlem  19701  0ringnnzr  20042  assamulgscm  20130  gsumply1subr  20402  gsummoncoe1  20472  pf1ind  20518  cnfldmulg  20577  cnfldexp  20578  psgndiflemB  20744  matmulcell  21054  mat1dimscm  21084  dmatmul  21106  dmatscmcl  21112  scmataddcl  21125  scmatsubcl  21126  scmatsgrp1  21131  mavmulsolcl  21160  ma1repveval  21180  1marepvmarrepid  21184  symgmatr01lem  21262  slesolvec  21288  cramerimplem2  21293  decpmatmullem  21379  pm2mpf1  21407  mp2pm2mplem4  21417  monmat2matmon  21432  chpscmat  21450  chpscmatgsumbin  21452  fvmptnn04ifb  21459  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  cpmadugsumlemF  21484  toprntopon  21533  clsss  21662  ntrss  21663  restntr  21790  cmpsublem  22007  cmpsub  22008  2ndcrest  22062  txindislem  22241  t0kq  22426  filufint  22528  fbflim2  22585  flftg  22604  alexsubALTlem4  22658  cnextfvval  22673  ustuqtop4  22853  xmettri2  22950  mettri  22962  metss  23118  tngngp3  23265  clmvscom  23694  lmmbr  23861  caublcls  23912  lmcau  23916  ovolunlem1a  24097  nulmbl2  24137  voliunlem1  24151  iunmbl  24154  volsup  24157  dvlip  24590  dvfsumle  24618  degltlem1  24666  ply1divex  24730  plyco  24831  dgrnznn  24837  dvnply2  24876  plydivex  24886  aannenlem2  24918  aaliou3lem2  24932  ulmcau  24983  zabsle1  25872  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  gausslemma2dlem3  25944  gausslemma2dlem4  25945  2lgslem1a1  25965  2sqnn0  26014  2sqreulem1  26022  2sqreunnlem1  26025  dchrisumlem1  26065  dchrisumlem2  26066  dchrisumlem3  26067  qabvle  26201  ostthlem2  26204  ostth2lem2  26210  tgjustr  26260  axeuclidlem  26748  incistruhgr  26864  umgredgprv  26892  umgrpredgv  26925  usgredgprvALT  26977  uhgr2edg  26990  usgredg2vlem2  27008  lfuhgr1v0e  27036  subgrfun  27063  umgrres1lem  27092  upgrres1  27095  fusgrfis  27112  uhgrnbgr0nb  27136  nbgr1vtx  27140  nb3grprlem1  27162  uvtx01vtx  27179  fusgrn0degnn0  27281  vtxdginducedm1lem4  27324  finsumvtxdg2size  27332  wlkl1loop  27419  wlkres  27452  lfgrwlknloop  27471  pthdadjvtx  27511  upgr2pthnlp  27513  upgrwlkdvdelem  27517  upgrwlkdvde  27518  uhgrwkspthlem2  27535  usgr2trlspth  27542  usgr2pth  27545  pthdlem2lem  27548  lfgrn1cycl  27583  uspgrn2crct  27586  crctcshwlkn0lem3  27590  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  iswspthsnon  27634  wlkiswwlks1  27645  wlklnwwlkln1  27646  wlkiswwlks2  27653  wlkiswwlksupgr2  27655  wlklnwwlkln2lem  27660  wlknwwlksnbij  27666  wwlksnred  27670  wwlksnext  27671  wwlksnredwwlkn  27673  wwlksnredwwlkn0  27674  wwlksnextfun  27676  wwlksnextinj  27677  wwlksnextsurj  27678  wspthsnonn0vne  27696  wspn0  27703  wwlks2onv  27732  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlk  27754  clwwlkccatlem  27767  clwlkclwwlklem2a1  27770  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a4  27775  clwlkclwwlklem2a  27776  clwlkclwwlklem2  27778  clwlkclwwlkf1lem3  27784  clwwisshclwwslem  27792  clwwisshclwwsn  27794  erclwwlktr  27800  isclwwlknx  27814  clwwlkinwwlk  27818  clwwlkel  27825  clwwlkf  27826  clwwlkf1  27828  clwwlkfo  27829  clwwlkext2edg  27835  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  clwwlknscsh  27841  erclwwlkntr  27850  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwwlknon0  27872  clwwlknonel  27874  clwwlknon1  27876  clwwlknonwwlknonb  27885  clwwlknonex2lem2  27887  clwwlknun  27891  clwwlkvbij  27892  upgr3v3e3cycl  27959  uhgr3cyclex  27961  upgr4cycl4dv4e  27964  eulerpath  28020  eucrctshift  28022  eucrct2eupth  28024  1to2vfriswmgr  28058  1to3vfriswmgr  28059  3cyclfrgrrn1  28064  4cycl2vnunb  28069  frgrwopreglem2  28092  frgrwopreglem3  28093  frgrwopreglem5ALT  28101  fusgr2wsp2nb  28113  2clwwlk2clwwlklem  28125  2clwwlk2clwwlk  28129  numclwwlk1lem2f1  28136  numclwwlk1lem2fo  28137  numclwwlk1  28140  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  numclwlk1  28150  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  numclwwlk5  28167  frgrreg  28173  frgrregord013  28174  friendship  28178  nsnlplig  28258  nsnlpligALT  28259  isgrpo  28274  vcdi  28342  vcdir  28343  vcass  28344  nmosetre  28541  hlim2  28969  shscli  29094  chintcli  29108  dfch2  29184  spansncvi  29429  nmopsetretALT  29640  nmfnsetre  29654  lnopl  29691  lnfnl  29708  pjss2coi  29941  pjorthcoi  29946  pjscji  29947  pjssdif2i  29951  pjclem4a  29975  pj3lem1  29983  strlem5  30032  hstrlem5  30040  cvmdi  30101  mdslmd3i  30109  atcv1  30157  atcvat4i  30174  cdj3lem2a  30213  cdj3lem3a  30216  opreu2reuALT  30240  iuninc  30312  disji2f  30327  disjif2  30331  fmptcof2  30402  xrsmulgzz  30665  ofldchr  30887  esumfzf  31328  issgon  31382  voliune  31488  volfiniune  31489  rrvsum  31712  bnj228  32005  bnj1294  32089  bnj229  32156  bnj607  32188  bnj908  32203  bnj953  32211  bnj1118  32256  bnj1174  32275  bnj1388  32305  funen1cnv  32357  acycgrsubgr  32405  cvmliftlem15  32545  satfsschain  32611  satfdm  32616  satf0op  32624  fmla0xp  32630  gonarlem  32641  goalrlem  32643  satffunlem1lem1  32649  satffunlem2lem1  32651  dmopab3rexdif  32652  satefvfmla0  32665  prv1n  32678  iprodefisumlem  32972  faclimlem1  32975  dfon2lem6  33033  tfisg  33055  poseq  33095  frrlem8  33130  fpr2  33140  frr2  33145  noprefixmo  33202  nosupbnd1lem5  33212  nocvxminlem  33247  nocvxmin  33248  slerec  33277  idinside  33545  onsucconni  33785  axc11n11r  34017  bj-brrelex12ALT  34362  bj-snmoore  34408  bj-finsumval0  34570  exlimim  34626  exellim  34628  icoreclin  34641  difunieq  34658  fvineqsneq  34696  pibt2  34701  wl-spae  34776  wl-aleq  34790  fin2so  34894  matunitlindf  34905  poimirlem4  34911  poimirlem26  34933  itg2addnclem  34958  upixp  35019  welb  35026  sdclem2  35032  metf1o  35045  sstotbnd3  35069  isbndx  35075  ismtycnv  35095  heiborlem4  35107  bfplem1  35115  opidonOLD  35145  grpomndo  35168  ax12eq  36092  ax12el  36093  cvrat4  36594  mzpexpmpt  39391  diophren  39459  rmxypos  39593  jm2.17a  39606  jm2.17b  39607  rmygeid  39610  jm2.18  39634  jm2.25  39645  jm2.15nn0  39649  jm2.16nn0  39650  pwslnm  39743  isnumbasgrplem1  39750  dgraalem  39794  relexpiidm  40098  relexpmulnn  40103  relexpmulg  40104  relexp01min  40107  relexp0a  40110  relexpxpmin  40111  clsk1indlem3  40442  grucollcld  40645  dvgrat  40693  radcnvrat  40695  sspwimpcf  41303  sspwimpcfVD  41304  e2ebindALT  41312  eu2ndop1stv  43373  afvfv0bi  43400  afveu  43401  afvres  43420  aovmpt4g  43449  ndmaovass  43454  ndmaovdistr  43455  afv2orxorb  43476  afv2eu  43486  imarnf1pr  43530  nltle2tri  43562  fzopredsuc  43572  subsubelfzo0  43575  fzoopth  43576  2ffzoeq  43577  smonoord  43580  elsetpreimafvssdm  43595  iccpartres  43627  iccpartiltu  43631  iccpartigtl  43632  iccpartgt  43636  icceuelpartlem  43644  fargshiftf1  43650  ichnreuop  43683  ichreuopeq  43684  elsprel  43686  sprsymrelfo  43708  prproropf1olem4  43717  paireqne  43722  sbcpr  43732  reupr  43733  goldbachth  43758  fmtnoprmfac1  43776  fmtnoprmfac2  43778  prmdvdsfmtnof1lem2  43796  lighneallem2  43820  lighneallem4  43824  requad2  43837  even3prm2  43933  fpprwpprb  43954  gbegt5  43975  sbgoldbwt  43991  sbgoldbm  43998  nnsum3primesgbe  44006  wtgoldbnnsum4prm  44016  bgoldbnnsum3prm  44018  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  isomuspgrlem1  44041  isomuspgrlem2d  44045  upgrwlkupwlk  44064  uspgropssxp  44068  uspgrsprfo  44072  mgmpropd  44091  isassintop  44166  lidldomn1  44241  lidlmmgm  44245  2zlidl  44254  2zrngamgm  44259  2zrngmmgm  44266  rnghmsscmap  44294  rnghmsubcsetclem2  44296  rngcinv  44301  rngccatidALTV  44309  rngcinvALTV  44313  funcrngcsetc  44318  funcrngcsetcALT  44319  rhmsscmap  44340  rhmsubcsetclem2  44342  rhmsubcrngclem2  44348  ringcinv  44352  funcringcsetc  44355  funcringcsetcALTV2lem9  44364  ringccatidALTV  44372  ringcinvALTV  44376  srhmsubc  44396  rhmsubclem4  44409  srhmsubcALTV  44414  rhmsubcALTVlem4  44427  lmodvsmdi  44479  ply1mulgsumlem1  44489  ply1mulgsumlem2  44490  lincdifsn  44528  lincsumcl  44535  lincscmcl  44536  lincext3  44560  lindslinindsimp1  44561  lindslinindsimp2lem5  44566  snlindsntor  44575  lincresunit2  44582  lincresunit3lem2  44584  zgtp1leeq  44625  m1modmmod  44630  elbigo2  44661  fllog2  44677  digexp  44716  dig1  44717  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  rrxlinec  44772  eenglngeehlnm  44775  rrx2linest  44778  itsclc0yqsol  44800  itsclc0xyqsol  44804