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  2240  nfsb4t  2501  mo4  2563  2euexv  2628  2euex  2638  raleqbidvvOLD  3302  gencl  3479  2gencl  3480  vtocl2ga  3530  vtocl2gaf  3531  vtocl3gaf  3533  vtocl3ga  3535  vtocl4g  3537  vtocl4ga  3538  rspccva  3572  2reurex  3715  2reu1  3844  rexdifi  4099  sseq0  4352  r19.2z  4449  falseral0OLD  4465  elelpwi  4561  preqsnd  4812  prproe  4858  ssuni  4885  disji2  5079  disjiun  5083  disjxiun  5092  trintss  5220  ssexg  5265  reusv2lem3  5342  propeqop  5452  otiunsndisj  5465  rexopabb  5473  pofun  5547  solin  5556  2optocl  5717  3optocl  5718  ssrelrn  5840  elrnmpt1  5906  resieq  5946  imadifssran  6106  reuop  6248  fnun  6603  fss  6675  fun  6693  fvelimab  6903  fvmptss  6950  fvn0ssdmfun  7016  fvcofneq  7035  fmptco  7071  funsndifnop  7093  fnressn  7100  fressnfv  7102  fmptsng  7111  fvtp2g  7142  fvtp3g  7143  tpres  7144  fnex  7160  funfvima3  7179  fvf1pr  7250  isores3  7278  tfisg  7793  dmfex  7844  opreuopreu  7975  releldmdifi  7986  funeldmdif  7989  el2mpocsbcl  8024  f1o2ndf1  8061  frxp  8065  fnse  8072  frxp2  8083  frxp3  8090  poseq  8097  ressuppssdif  8124  funsssuppss  8129  mpoxopxnop0  8154  reldmtpos  8173  frrlem8  8232  fpr2a  8241  smores  8281  tfrlem7  8311  tz7.48-2  8370  tz7.49  8373  oacl  8459  omcl  8460  oecl  8461  oarec  8486  oewordri  8516  oeworde  8517  oelim2  8519  oeoa  8521  oeoelem  8522  oeoe  8523  nnacl  8535  nnmcl  8536  nnecl  8537  nnmsucr  8549  naddoa  8626  brinxper  8660  2ecoptocl  8741  fsetprcnex  8795  undifixp  8868  xpf1o  9063  limensuc  9078  unfi  9091  en1eqsn  9170  ac6sfi  9179  frfi  9180  difinf  9206  imafiOLD  9211  f1dmvrnfibi  9236  f1vrnfibi  9237  suppeqfsuppbi  9274  elfiun  9325  dffi3  9326  infsupprpr  9401  xpwdomg  9482  infdiffi  9559  ttrclselem2  9627  epfrs  9632  frmin  9653  frr2  9664  rankxpsuc  9786  updjud  9838  tskwe  9854  infxpenlem  9915  fseqenlem1  9926  kmlem2  10054  nnadju  10100  cff1  10160  cflim2  10165  sornom  10179  infpssrlem4  10208  fin23lem26  10227  fin23lem30  10244  fin23lem34  10248  isf32lem11  10265  fin67  10297  isfin7-2  10298  fin1a2lem10  10311  axcc2lem  10338  axdc2lem  10350  axdc3lem2  10353  axdc3lem4  10355  axdc4lem  10357  iunfo  10441  tsk0  10665  gruina  10720  grur1a  10721  mulcanenq  10862  reclem2pr  10950  supsrlem  11013  supsr  11014  ax1rid  11063  negf1o  11558  mulgt1OLD  11991  lbreu  12083  nnindd  12156  nnaddcl  12159  nnmulcl  12160  nn0n0n1ge2b  12461  nn0indd  12580  fzind  12581  fnn0ind  12582  uzaddcl  12808  uzinfi  12832  nn01to3  12845  elpq  12879  xmulasslem2  13188  supxrunb1  13225  supxrunb2  13226  infmremnf  13250  infmrp1  13251  uzsubsubfz  13453  fzdif1  13512  elfz0ubfz0  13539  fz0fzdiffz0  13544  elfzmlbp  13546  fzofzim  13616  elfzom1elp1fzo  13639  ssfzo12bi  13668  fzoopth  13669  fzonfzoufzol  13678  elfznelfzob  13681  injresinjlem  13697  injresinj  13698  modaddmodup  13848  modfzo0difsn  13857  modsumfzodifsn  13858  addmodlteq  13860  om2uzlti  13864  fsequb  13889  ssnn0fi  13899  ser1const  13972  expcllem  13986  expeq0  14006  expmordi  14081  expnngt1  14155  faclbnd  14204  hashf1rn  14266  hashgadd  14291  hashunx  14300  hashnn0n0nn  14305  hashgt0elex  14315  hashss  14323  hashfzp1  14345  hashxp  14348  hashmap  14349  hashimarni  14355  seqcoll  14378  hash2exprb  14385  hashge2el2difr  14395  elss2prb  14402  hashdifsnp1  14420  fi1uzind  14421  brfi1indALT  14424  lswlgt0cl  14483  swrdnd  14569  swrdnnn0nd  14571  swrdnd0  14572  swrd0  14573  swrdsbslen  14579  swrdspsleq  14580  pfxsuff1eqwrdeq  14613  swrdswrdlem  14618  swrdswrd  14619  wrd2ind  14637  pfxccatin12lem2a  14641  swrdccatin2  14643  pfxccatin12lem2  14645  pfxccatin12lem3  14646  pfxccatin12  14647  pfxccat3  14648  swrdccat  14649  pfxccat3a  14652  swrdccat3blem  14653  repswswrd  14698  repswrevw  14701  cshwmodn  14709  cshwsublen  14710  cshwidxmod  14717  cshwidxmodr  14718  cshf1  14724  2cshw  14727  cshweqrep  14735  cshw1  14736  2cshwcshw  14739  cshwcshid  14741  cshwcsh2id  14742  wrdlen2i  14856  2swrd2eqwrdeq  14867  wwlktovfo  14872  relexpsucnnl  14944  rtrclreclem3  14974  rtrclreclem4  14975  relexpindlem  14977  r19.29uz  15265  caubnd  15273  sqreu  15275  climshft  15490  climub  15576  climserle  15577  sumss  15638  sumss2  15640  modfsummods  15707  o1fsum  15727  binom  15744  climcndslem1  15763  climcndslem2  15764  cvgrat  15797  clim2prod  15802  prodfn0  15808  prodfrec  15809  ntrivcvgfvn0  15813  fprodn0  15893  fprodmodd  15911  fprodefsum  16009  demoivreALT  16117  ruclem8  16153  dvdsaddre2b  16225  dvdsdivcl  16234  dvdsfac  16244  oddnn02np1  16266  oddge22np1  16267  evennn02n  16268  evennn2n  16269  m1exp1  16294  nn0o  16301  pwp1fsum  16309  flodddiv4  16333  smu01lem  16403  dvdslegcd  16422  gcdneg  16440  dfgcd2  16464  seq1st  16489  alginv  16493  lcmf  16551  lcmftp  16554  lcmfunsnlem2lem2  16557  lcmfunsnlem  16559  lcmfun  16563  ncoprmgcdne1b  16568  coprmproddvdslem  16580  coprmproddvds  16581  cncongr1  16585  prmdvdsexp  16633  prmndvdsfaclt  16643  ncoprmlnprm  16646  fvprmselgcd1  16964  prmgaplem6  16975  prmgaplem7  16976  prmgaplem8  16977  cshwshashlem1  17014  setsstruct2  17092  setsstruct  17094  inveq  17689  catsubcat  17754  initoeu2lem0  17928  initoeu2lem1  17929  funcestrcsetclem8  18061  funcestrcsetclem9  18062  fthestrcsetc  18064  fullestrcsetc  18065  funcsetcestrclem9  18077  fthsetcestrc  18079  fullsetcestrc  18080  lubss  18427  lubel  18428  mgmpropd  18567  issstrmgm  18569  mgmb1mgm1  18571  sgrpidmnd  18655  frmdgsum  18778  smndex1mndlem  18825  mgm2nsgrplem3  18836  dfgrp2  18883  cyccom  19123  gaass  19217  gsumwrev  19286  symgextf1lem  19340  symgextf1  19341  fvcosymgeq  19349  gsmsymgreq  19352  symgfixelsi  19355  pmtrprfv3  19374  symggen  19390  pmtrprfval  19407  gsumzres  19829  gsumpr  19875  gsumzunsnd  19876  srgmulgass  20143  srgbinom  20157  0ringnnzr  20449  rnghmsscmap  20554  rnghmsubcsetclem2  20556  rngcinv  20561  funcrngcsetc  20564  funcrngcsetcALT  20565  rhmsscmap  20583  rhmsubcsetclem2  20585  rhmsubcrngclem2  20591  funcringcsetc  20598  srhmsubc  20604  rhmsubclem4  20612  lmodvsmmulgdi  20839  lmodfopnelem1  20840  rmodislmodlem  20871  rngqiprngimfo  21247  cnfldmulg  21349  cnfldexp  21350  ofldchr  21522  psgndiflemB  21546  assamulgscm  21848  gsumply1subr  22165  gsummoncoe1  22243  pf1ind  22290  matmulcell  22380  mat1dimscm  22410  dmatmul  22432  dmatscmcl  22438  scmataddcl  22451  scmatsubcl  22452  scmatsgrp1  22457  mavmulsolcl  22486  ma1repveval  22506  1marepvmarrepid  22510  symgmatr01lem  22588  slesolvec  22614  cramerimplem2  22619  decpmatmullem  22706  pm2mpf1  22734  mp2pm2mplem4  22744  monmat2matmon  22759  chpscmat  22777  chpscmatgsumbin  22779  fvmptnn04ifb  22786  chfacfscmul0  22793  chfacfscmulgsum  22795  chfacfpmmul0  22797  chfacfpmmulgsum  22799  cpmadugsumlemF  22811  toprntopon  22860  clsss  22989  ntrss  22990  restntr  23117  cmpsublem  23334  cmpsub  23335  2ndcrest  23389  txindislem  23568  t0kq  23753  filufint  23855  fbflim2  23912  flftg  23931  alexsubALTlem4  23985  cnextfvval  24000  ustuqtop4  24179  xmettri2  24275  mettri  24287  metss  24443  tngngp3  24591  clmvscom  25037  lmmbr  25205  caublcls  25256  lmcau  25260  ovolunlem1a  25444  nulmbl2  25484  voliunlem1  25498  iunmbl  25501  volsup  25504  dvlip  25945  dvfsumle  25973  dvfsumleOLD  25974  degltlem1  26024  ply1divex  26089  plyco  26193  dgrnznn  26199  dvnply2  26242  plydivex  26252  aannenlem2  26284  aaliou3lem2  26298  ulmcau  26351  zabsle1  27254  gausslemma2dlem1a  27323  gausslemma2dlem2  27325  gausslemma2dlem3  27326  gausslemma2dlem4  27327  2lgslem1a1  27347  2sqnn0  27396  2sqreulem1  27404  2sqreunnlem1  27407  dchrisumlem1  27447  dchrisumlem2  27448  dchrisumlem3  27449  qabvle  27583  ostthlem2  27586  ostth2lem2  27592  nosupbnd1lem5  27671  noinfbnd1lem5  27686  nocvxminlem  27737  slerec  27780  madebdaylemold  27863  mulsuniflem  28108  precsexlem6  28170  precsexlem7  28171  precsexlem8  28172  precsexlem9  28173  abssge0  28203  noseqind  28242  om2noseqlt  28249  om2noseqrdg  28254  n0addscl  28292  n0mulscl  28293  onsfi  28303  expscllem  28373  pw2cut2  28402  zs12zodd  28412  tgjustr  28472  axeuclidlem  28961  incistruhgr  29078  umgredgprv  29106  umgrpredgv  29139  usgredgprvALT  29194  uhgr2edg  29207  usgredg2vlem2  29225  lfuhgr1v0e  29253  subgrfun  29280  umgrres1lem  29309  upgrres1  29312  fusgrfis  29329  uhgrnbgr0nb  29353  nbgr1vtx  29357  nb3grprlem1  29379  uvtx01vtx  29396  fusgrn0degnn0  29499  vtxdginducedm1lem4  29542  finsumvtxdg2size  29550  wlkl1loop  29637  wlkres  29668  lfgrwlknloop  29687  pthdadjvtx  29727  dfpth2  29728  upgr2pthnlp  29731  upgrwlkdvdelem  29735  upgrwlkdvde  29736  uhgrwkspthlem2  29753  usgr2trlspth  29760  usgr2pth  29763  pthdlem2lem  29766  cyclnumvtx  29799  lfgrn1cycl  29804  uspgrn2crct  29807  crctcshwlkn0lem3  29811  crctcshwlkn0lem4  29812  crctcshwlkn0lem5  29813  iswspthsnon  29855  wlkiswwlks1  29866  wlklnwwlkln1  29867  wlkiswwlks2  29874  wlkiswwlksupgr2  29876  wlklnwwlkln2lem  29881  wlknwwlksnbij  29887  wwlksnred  29891  wwlksnext  29892  wwlksnredwwlkn  29894  wwlksnredwwlkn0  29895  wwlksnextfun  29897  wwlksnextinj  29898  wwlksnextsurj  29899  wspthsnonn0vne  29916  wspn0  29923  wwlks2onv  29952  elwwlks2  29968  elwspths2spth  29969  rusgrnumwwlk  29977  clwwlkccatlem  29990  clwlkclwwlklem2a1  29993  clwlkclwwlklem2fv2  29997  clwlkclwwlklem2a4  29998  clwlkclwwlklem2a  29999  clwlkclwwlklem2  30001  clwlkclwwlkf1lem3  30007  clwwisshclwwslem  30015  clwwisshclwwsn  30017  erclwwlktr  30023  isclwwlknx  30037  clwwlkinwwlk  30041  clwwlkel  30047  clwwlkf  30048  clwwlkf1  30050  clwwlkfo  30051  clwwlkext2edg  30057  wwlksext2clwwlk  30058  wwlksubclwwlk  30059  clwwlknscsh  30063  erclwwlkntr  30072  eleclclwwlkn  30077  hashecclwwlkn1  30078  umgrhashecclwwlk  30079  clwwlknon0  30094  clwwlknonel  30096  clwwlknon1  30098  clwwlknonwwlknonb  30107  clwwlknonex2lem2  30109  clwwlknun  30113  clwwlkvbij  30114  upgr3v3e3cycl  30181  uhgr3cyclex  30183  upgr4cycl4dv4e  30186  eulerpath  30242  eucrctshift  30244  eucrct2eupth  30246  1to2vfriswmgr  30280  1to3vfriswmgr  30281  3cyclfrgrrn1  30286  4cycl2vnunb  30291  frgrwopreglem2  30314  frgrwopreglem3  30315  frgrwopreglem5ALT  30323  fusgr2wsp2nb  30335  2clwwlk2clwwlklem  30347  2clwwlk2clwwlk  30351  numclwwlk1lem2f1  30358  numclwwlk1lem2fo  30359  numclwwlk1  30362  clwwlknonclwlknonf1o  30363  dlwwlknondlwlknonf1o  30366  numclwlk1  30372  numclwlk2lem2f  30378  numclwlk2lem2f1o  30380  numclwwlk5  30389  frgrreg  30395  frgrregord013  30396  friendship  30400  nsnlplig  30482  nsnlpligALT  30483  isgrpo  30498  vcdi  30566  vcdir  30567  vcass  30568  nmosetre  30765  hlim2  31193  shscli  31318  chintcli  31332  dfch2  31408  spansncvi  31653  nmopsetretALT  31864  nmfnsetre  31878  lnopl  31915  lnfnl  31932  pjss2coi  32165  pjorthcoi  32170  pjscji  32171  pjssdif2i  32175  pjclem4a  32199  pj3lem1  32207  strlem5  32256  hstrlem5  32264  cvmdi  32325  mdslmd3i  32333  atcv1  32381  atcvat4i  32398  cdj3lem2a  32437  cdj3lem3a  32440  opreu2reuALT  32477  iuninc  32561  disji2f  32578  disjif2  32582  fmptcof2  32661  xrsmulgzz  33019  1arithufdlem3  33555  esumfzf  34154  issgon  34208  voliune  34314  volfiniune  34315  rrvsum  34539  bnj228  34819  bnj1294  34901  bnj229  34968  bnj607  35000  bnj908  35015  bnj953  35023  bnj1118  35068  bnj1174  35087  bnj1388  35117  funen1cnv  35172  rankfilimbi  35184  r1filimi  35186  trssfir1om  35194  trssfir1omregs  35204  acycgrsubgr  35274  cvmliftlem15  35414  satfsschain  35480  satfdm  35485  satf0op  35493  fmla0xp  35499  gonarlem  35510  goalrlem  35512  satffunlem1lem1  35518  satffunlem2lem1  35520  dmopab3rexdif  35521  satefvfmla0  35534  prv1n  35547  iprodefisumlem  35856  faclimlem1  35859  dfon2lem6  35902  idinside  36200  onsucconni  36553  axc11n11r  36800  bj-brrelex12ALT  37184  bj-snmoore  37230  bj-finsumval0  37402  exlimim  37459  exellim  37461  icoreclin  37474  difunieq  37491  fvineqsneq  37529  pibt2  37534  wl-spae  37638  wl-aleq  37652  fin2so  37720  matunitlindf  37731  poimirlem4  37737  poimirlem26  37759  itg2addnclem  37784  upixp  37842  welb  37849  sdclem2  37855  metf1o  37868  sstotbnd3  37889  isbndx  37895  ismtycnv  37915  heiborlem4  37927  bfplem1  37935  opidonOLD  37965  grpomndo  37988  ax12eq  39113  ax12el  39114  cvrat4  39615  nn0addcom  42632  nn0mulcom  42636  mzpexpmpt  42902  diophren  42970  rmxypos  43104  jm2.17a  43117  jm2.17b  43118  rmygeid  43121  jm2.18  43145  jm2.25  43156  jm2.15nn0  43160  jm2.16nn0  43161  pwslnm  43251  isnumbasgrplem1  43258  dgraalem  43302  onuniintrab  43383  onsupuni  43386  onsupcl3  43390  naddonnn  43552  naddwordnexlem2  43555  relexpiidm  43861  relexpmulnn  43866  relexpmulg  43867  relexp01min  43870  relexp0a  43873  relexpxpmin  43874  clsk1indlem3  44200  grucollcld  44417  dvgrat  44469  radcnvrat  44471  sspwimpcf  45076  sspwimpcfVD  45077  e2ebindALT  45085  trfr  45119  et-sqrtnegnre  47033  fsetprcnexALT  47224  eu2ndop1stv  47287  afvfv0bi  47314  afveu  47315  afvres  47334  aovmpt4g  47363  ndmaovass  47368  ndmaovdistr  47369  afv2orxorb  47390  afv2eu  47400  imarnf1pr  47444  nltle2tri  47475  fzopredsuc  47485  subsubelfzo0  47488  2ffzoeq  47489  2tceilhalfelfzo1  47494  m1modmmod  47520  smonoord  47533  elsetpreimafvssdm  47548  iccpartres  47580  iccpartiltu  47584  iccpartigtl  47585  iccpartgt  47589  icceuelpartlem  47597  fargshiftf1  47603  ichnreuop  47634  ichreuopeq  47635  elsprel  47637  sprsymrelfo  47659  prproropf1olem4  47668  paireqne  47673  sbcpr  47683  reupr  47684  goldbachth  47709  fmtnoprmfac1  47727  fmtnoprmfac2  47729  prmdvdsfmtnof1lem2  47747  lighneallem2  47768  lighneallem4  47772  requad2  47785  even3prm2  47881  fpprwpprb  47902  gbegt5  47923  sbgoldbwt  47939  sbgoldbm  47946  nnsum3primesgbe  47954  wtgoldbnnsum4prm  47964  bgoldbnnsum3prm  47966  bgoldbtbndlem2  47968  bgoldbtbndlem3  47969  bgoldbtbndlem4  47970  bgoldbtbnd  47971  isubgredg  48028  grimuhgr  48049  clnbgrgrim  48096  grtriprop  48103  cycl3grtrilem  48108  cycl3grtri  48109  gpgusgralem  48218  gpgedgvtx0  48223  gpgedgvtx1  48224  gpgcubic  48241  gpg5nbgr3star  48243  gpgprismgr4cycllem3  48259  upgrwlkupwlk  48302  uspgropssxp  48306  uspgrsprfo  48310  isassintop  48372  lidldomn1  48393  2zlidl  48402  2zrngamgm  48407  2zrngmmgm  48414  rngccatidALTV  48434  rngcinvALTV  48438  rhmsubcALTVlem4  48446  funcringcsetcALTV2lem9  48460  ringccatidALTV  48468  srhmsubcALTV  48487  lmodvsmdi  48541  ply1mulgsumlem1  48548  ply1mulgsumlem2  48549  lincdifsn  48586  lincsumcl  48593  lincscmcl  48594  lincext3  48618  lindslinindsimp1  48619  lindslinindsimp2lem5  48624  snlindsntor  48633  lincresunit2  48640  lincresunit3lem2  48642  zgtp1leeq  48683  elbigo2  48714  fllog2  48730  digexp  48769  dig1  48770  nn0sumshdiglemA  48781  nn0sumshdiglemB  48782  1arymaptf1  48804  2arymaptf1  48815  rrxlinec  48898  eenglngeehlnm  48901  rrx2linest  48904  itsclc0yqsol  48926  itsclc0xyqsol  48930