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  1874  19.41v  1949  19.41  2236  nfsb4t  2497  mo4  2559  2euexv  2624  2euex  2634  raleqbidvvOLD  3299  gencl  3480  2gencl  3481  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4g  3542  vtocl4ga  3543  rspccva  3578  2reurex  3722  2reu1  3851  rexdifi  4103  sseq0  4356  r19.2z  4448  ralf0  4467  falseral0  4469  elelpwi  4563  preqsnd  4813  prproe  4859  ssuni  4886  disji2  5079  disjiun  5083  disjxiun  5092  trintss  5220  ssexg  5265  reusv2lem3  5342  propeqop  5454  otiunsndisj  5467  rexopabb  5475  pofun  5549  solin  5558  2optocl  5719  3optocl  5720  ssrelrn  5841  elrnmpt1  5906  resieq  5945  imadifssran  6104  reuop  6245  fnun  6600  fss  6672  fun  6690  fvelimab  6899  fvmptss  6946  fvn0ssdmfun  7012  fvcofneq  7031  fmptco  7067  funsndifnop  7089  fnressn  7096  fressnfv  7098  fvn0fvelrnOLD  7101  fmptsng  7108  fvtp2g  7139  fvtp3g  7140  tpres  7141  fnex  7157  funfvima3  7176  fvf1pr  7248  isores3  7276  tfisg  7794  dmfex  7845  opreuopreu  7976  releldmdifi  7987  funeldmdif  7990  el2mpocsbcl  8025  f1o2ndf1  8062  frxp  8066  fnse  8073  frxp2  8084  frxp3  8091  poseq  8098  ressuppssdif  8125  funsssuppss  8130  mpoxopxnop0  8155  reldmtpos  8174  frrlem8  8233  fpr2a  8242  smores  8282  tfrlem7  8312  tz7.48-2  8371  tz7.49  8374  oacl  8460  omcl  8461  oecl  8462  oarec  8487  oewordri  8517  oeworde  8518  oelim2  8520  oeoa  8522  oeoelem  8523  oeoe  8524  nnacl  8536  nnmcl  8537  nnecl  8538  nnmsucr  8550  naddoa  8627  brinxper  8661  2ecoptocl  8742  fsetprcnex  8796  undifixp  8868  xpf1o  9063  limensuc  9078  unfi  9095  en1eqsn  9177  ac6sfi  9189  frfi  9190  difinf  9218  imafiOLD  9223  f1dmvrnfibi  9250  f1vrnfibi  9251  suppeqfsuppbi  9288  elfiun  9339  dffi3  9340  infsupprpr  9415  xpwdomg  9496  infdiffi  9573  ttrclselem2  9641  epfrs  9646  frmin  9664  frr2  9675  rankxpsuc  9797  updjud  9849  tskwe  9865  infxpenlem  9926  fseqenlem1  9937  kmlem2  10065  nnadju  10111  cff1  10171  cflim2  10176  sornom  10190  infpssrlem4  10219  fin23lem26  10238  fin23lem30  10255  fin23lem34  10259  isf32lem11  10276  fin67  10308  isfin7-2  10309  fin1a2lem10  10322  axcc2lem  10349  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  iunfo  10452  tsk0  10676  gruina  10731  grur1a  10732  mulcanenq  10873  reclem2pr  10961  supsrlem  11024  supsr  11025  ax1rid  11074  negf1o  11569  mulgt1OLD  12002  lbreu  12094  nnindd  12167  nnaddcl  12170  nnmulcl  12171  nn0n0n1ge2b  12472  nn0indd  12592  fzind  12593  fnn0ind  12594  uzaddcl  12824  uzinfi  12848  nn01to3  12861  elpq  12895  xmulasslem2  13203  supxrunb1  13240  supxrunb2  13241  infmremnf  13265  infmrp1  13266  uzsubsubfz  13468  fzdif1  13527  elfz0ubfz0  13554  fz0fzdiffz0  13559  elfzmlbp  13561  fzofzim  13631  elfzom1elp1fzo  13654  ssfzo12bi  13683  fzoopth  13684  fzonfzoufzol  13692  elfznelfzob  13695  injresinjlem  13709  injresinj  13710  modaddmodup  13860  modfzo0difsn  13869  modsumfzodifsn  13870  addmodlteq  13872  om2uzlti  13876  fsequb  13901  ssnn0fi  13911  ser1const  13984  expcllem  13998  expeq0  14018  expmordi  14093  expnngt1  14167  faclbnd  14216  hashf1rn  14278  hashgadd  14303  hashunx  14312  hashnn0n0nn  14317  hashgt0elex  14327  hashss  14335  hashfzp1  14357  hashxp  14360  hashmap  14361  hashimarni  14367  seqcoll  14390  hash2exprb  14397  hashge2el2difr  14407  elss2prb  14414  hashdifsnp1  14432  fi1uzind  14433  brfi1indALT  14436  lswlgt0cl  14495  swrdnd  14580  swrdnnn0nd  14582  swrdnd0  14583  swrd0  14584  swrdsbslen  14590  swrdspsleq  14591  pfxsuff1eqwrdeq  14624  swrdswrdlem  14629  swrdswrd  14630  wrd2ind  14648  pfxccatin12lem2a  14652  swrdccatin2  14654  pfxccatin12lem2  14656  pfxccatin12lem3  14657  pfxccatin12  14658  pfxccat3  14659  swrdccat  14660  pfxccat3a  14663  swrdccat3blem  14664  repswswrd  14709  repswrevw  14712  cshwmodn  14720  cshwsublen  14721  cshwidxmod  14728  cshwidxmodr  14729  cshf1  14735  2cshw  14738  cshweqrep  14746  cshw1  14747  2cshwcshw  14751  cshwcshid  14753  cshwcsh2id  14754  wrdlen2i  14868  2swrd2eqwrdeq  14879  wwlktovfo  14884  relexpsucnnl  14956  rtrclreclem3  14986  rtrclreclem4  14987  relexpindlem  14989  r19.29uz  15277  caubnd  15285  sqreu  15287  climshft  15502  climub  15588  climserle  15589  sumss  15650  sumss2  15652  modfsummods  15719  o1fsum  15739  binom  15756  climcndslem1  15775  climcndslem2  15776  cvgrat  15809  clim2prod  15814  prodfn0  15820  prodfrec  15821  ntrivcvgfvn0  15825  fprodn0  15905  fprodmodd  15923  fprodefsum  16021  demoivreALT  16129  ruclem8  16165  dvdsaddre2b  16237  dvdsdivcl  16246  dvdsfac  16256  oddnn02np1  16278  oddge22np1  16279  evennn02n  16280  evennn2n  16281  m1exp1  16306  nn0o  16313  pwp1fsum  16321  flodddiv4  16345  smu01lem  16415  dvdslegcd  16434  gcdneg  16452  dfgcd2  16476  seq1st  16501  alginv  16505  lcmf  16563  lcmftp  16566  lcmfunsnlem2lem2  16569  lcmfunsnlem  16571  lcmfun  16575  ncoprmgcdne1b  16580  coprmproddvdslem  16592  coprmproddvds  16593  cncongr1  16597  prmdvdsexp  16645  prmndvdsfaclt  16655  ncoprmlnprm  16658  fvprmselgcd1  16976  prmgaplem6  16987  prmgaplem7  16988  prmgaplem8  16989  cshwshashlem1  17026  setsstruct2  17104  setsstruct  17106  inveq  17700  catsubcat  17765  initoeu2lem0  17939  initoeu2lem1  17940  funcestrcsetclem8  18072  funcestrcsetclem9  18073  fthestrcsetc  18075  fullestrcsetc  18076  funcsetcestrclem9  18088  fthsetcestrc  18090  fullsetcestrc  18091  lubss  18438  lubel  18439  mgmpropd  18544  issstrmgm  18546  mgmb1mgm1  18548  sgrpidmnd  18632  frmdgsum  18755  smndex1mndlem  18802  mgm2nsgrplem3  18813  dfgrp2  18860  cyccom  19101  gaass  19195  gsumwrev  19264  symgextf1lem  19318  symgextf1  19319  fvcosymgeq  19327  gsmsymgreq  19330  symgfixelsi  19333  pmtrprfv3  19352  symggen  19368  pmtrprfval  19385  gsumzres  19807  gsumpr  19853  gsumzunsnd  19854  srgmulgass  20121  srgbinom  20135  0ringnnzr  20429  rnghmsscmap  20534  rnghmsubcsetclem2  20536  rngcinv  20541  funcrngcsetc  20544  funcrngcsetcALT  20545  rhmsscmap  20563  rhmsubcsetclem2  20565  rhmsubcrngclem2  20571  funcringcsetc  20578  srhmsubc  20584  rhmsubclem4  20592  lmodvsmmulgdi  20819  lmodfopnelem1  20820  rmodislmodlem  20851  rngqiprngimfo  21227  cnfldmulg  21329  cnfldexp  21330  ofldchr  21502  psgndiflemB  21526  assamulgscm  21827  gsumply1subr  22135  gsummoncoe1  22212  pf1ind  22259  matmulcell  22349  mat1dimscm  22379  dmatmul  22401  dmatscmcl  22407  scmataddcl  22420  scmatsubcl  22421  scmatsgrp1  22426  mavmulsolcl  22455  ma1repveval  22475  1marepvmarrepid  22479  symgmatr01lem  22557  slesolvec  22583  cramerimplem2  22588  decpmatmullem  22675  pm2mpf1  22703  mp2pm2mplem4  22713  monmat2matmon  22728  chpscmat  22746  chpscmatgsumbin  22748  fvmptnn04ifb  22755  chfacfscmul0  22762  chfacfscmulgsum  22764  chfacfpmmul0  22766  chfacfpmmulgsum  22768  cpmadugsumlemF  22780  toprntopon  22829  clsss  22958  ntrss  22959  restntr  23086  cmpsublem  23303  cmpsub  23304  2ndcrest  23358  txindislem  23537  t0kq  23722  filufint  23824  fbflim2  23881  flftg  23900  alexsubALTlem4  23954  cnextfvval  23969  ustuqtop4  24149  xmettri2  24245  mettri  24257  metss  24413  tngngp3  24561  clmvscom  25007  lmmbr  25175  caublcls  25226  lmcau  25230  ovolunlem1a  25414  nulmbl2  25454  voliunlem1  25468  iunmbl  25471  volsup  25474  dvlip  25915  dvfsumle  25943  dvfsumleOLD  25944  degltlem1  25994  ply1divex  26059  plyco  26163  dgrnznn  26169  dvnply2  26212  plydivex  26222  aannenlem2  26254  aaliou3lem2  26268  ulmcau  26321  zabsle1  27224  gausslemma2dlem1a  27293  gausslemma2dlem2  27295  gausslemma2dlem3  27296  gausslemma2dlem4  27297  2lgslem1a1  27317  2sqnn0  27366  2sqreulem1  27374  2sqreunnlem1  27377  dchrisumlem1  27417  dchrisumlem2  27418  dchrisumlem3  27419  qabvle  27553  ostthlem2  27556  ostth2lem2  27562  nosupbnd1lem5  27641  noinfbnd1lem5  27656  nocvxminlem  27707  slerec  27749  madebdaylemold  27831  mulsuniflem  28076  precsexlem6  28138  precsexlem7  28139  precsexlem8  28140  precsexlem9  28141  abssge0  28171  noseqind  28210  om2noseqlt  28217  om2noseqrdg  28222  n0addscl  28260  n0mulscl  28261  onsfi  28271  expscllem  28341  zs12zodd  28378  tgjustr  28438  axeuclidlem  28926  incistruhgr  29043  umgredgprv  29071  umgrpredgv  29104  usgredgprvALT  29159  uhgr2edg  29172  usgredg2vlem2  29190  lfuhgr1v0e  29218  subgrfun  29245  umgrres1lem  29274  upgrres1  29277  fusgrfis  29294  uhgrnbgr0nb  29318  nbgr1vtx  29322  nb3grprlem1  29344  uvtx01vtx  29361  fusgrn0degnn0  29464  vtxdginducedm1lem4  29507  finsumvtxdg2size  29515  wlkl1loop  29602  wlkres  29633  lfgrwlknloop  29652  pthdadjvtx  29692  dfpth2  29693  upgr2pthnlp  29696  upgrwlkdvdelem  29700  upgrwlkdvde  29701  uhgrwkspthlem2  29718  usgr2trlspth  29725  usgr2pth  29728  pthdlem2lem  29731  cyclnumvtx  29764  lfgrn1cycl  29769  uspgrn2crct  29772  crctcshwlkn0lem3  29776  crctcshwlkn0lem4  29777  crctcshwlkn0lem5  29778  iswspthsnon  29820  wlkiswwlks1  29831  wlklnwwlkln1  29832  wlkiswwlks2  29839  wlkiswwlksupgr2  29841  wlklnwwlkln2lem  29846  wlknwwlksnbij  29852  wwlksnred  29856  wwlksnext  29857  wwlksnredwwlkn  29859  wwlksnredwwlkn0  29860  wwlksnextfun  29862  wwlksnextinj  29863  wwlksnextsurj  29864  wspthsnonn0vne  29881  wspn0  29888  wwlks2onv  29917  elwwlks2  29930  elwspths2spth  29931  rusgrnumwwlk  29939  clwwlkccatlem  29952  clwlkclwwlklem2a1  29955  clwlkclwwlklem2fv2  29959  clwlkclwwlklem2a4  29960  clwlkclwwlklem2a  29961  clwlkclwwlklem2  29963  clwlkclwwlkf1lem3  29969  clwwisshclwwslem  29977  clwwisshclwwsn  29979  erclwwlktr  29985  isclwwlknx  29999  clwwlkinwwlk  30003  clwwlkel  30009  clwwlkf  30010  clwwlkf1  30012  clwwlkfo  30013  clwwlkext2edg  30019  wwlksext2clwwlk  30020  wwlksubclwwlk  30021  clwwlknscsh  30025  erclwwlkntr  30034  eleclclwwlkn  30039  hashecclwwlkn1  30040  umgrhashecclwwlk  30041  clwwlknon0  30056  clwwlknonel  30058  clwwlknon1  30060  clwwlknonwwlknonb  30069  clwwlknonex2lem2  30071  clwwlknun  30075  clwwlkvbij  30076  upgr3v3e3cycl  30143  uhgr3cyclex  30145  upgr4cycl4dv4e  30148  eulerpath  30204  eucrctshift  30206  eucrct2eupth  30208  1to2vfriswmgr  30242  1to3vfriswmgr  30243  3cyclfrgrrn1  30248  4cycl2vnunb  30253  frgrwopreglem2  30276  frgrwopreglem3  30277  frgrwopreglem5ALT  30285  fusgr2wsp2nb  30297  2clwwlk2clwwlklem  30309  2clwwlk2clwwlk  30313  numclwwlk1lem2f1  30320  numclwwlk1lem2fo  30321  numclwwlk1  30324  clwwlknonclwlknonf1o  30325  dlwwlknondlwlknonf1o  30328  numclwlk1  30334  numclwlk2lem2f  30340  numclwlk2lem2f1o  30342  numclwwlk5  30351  frgrreg  30357  frgrregord013  30358  friendship  30362  nsnlplig  30444  nsnlpligALT  30445  isgrpo  30460  vcdi  30528  vcdir  30529  vcass  30530  nmosetre  30727  hlim2  31155  shscli  31280  chintcli  31294  dfch2  31370  spansncvi  31615  nmopsetretALT  31826  nmfnsetre  31840  lnopl  31877  lnfnl  31894  pjss2coi  32127  pjorthcoi  32132  pjscji  32133  pjssdif2i  32137  pjclem4a  32161  pj3lem1  32169  strlem5  32218  hstrlem5  32226  cvmdi  32287  mdslmd3i  32295  atcv1  32343  atcvat4i  32360  cdj3lem2a  32399  cdj3lem3a  32402  opreu2reuALT  32440  iuninc  32523  disji2f  32540  disjif2  32544  fmptcof2  32619  xrsmulgzz  32982  1arithufdlem3  33502  esumfzf  34055  issgon  34109  voliune  34215  volfiniune  34216  rrvsum  34441  bnj228  34721  bnj1294  34803  bnj229  34870  bnj607  34902  bnj908  34917  bnj953  34925  bnj1118  34970  bnj1174  34989  bnj1388  35019  funen1cnv  35074  acycgrsubgr  35150  cvmliftlem15  35290  satfsschain  35356  satfdm  35361  satf0op  35369  fmla0xp  35375  gonarlem  35386  goalrlem  35388  satffunlem1lem1  35394  satffunlem2lem1  35396  dmopab3rexdif  35397  satefvfmla0  35410  prv1n  35423  iprodefisumlem  35732  faclimlem1  35735  dfon2lem6  35781  idinside  36077  onsucconni  36430  axc11n11r  36676  bj-brrelex12ALT  37060  bj-snmoore  37106  bj-finsumval0  37278  exlimim  37335  exellim  37337  icoreclin  37350  difunieq  37367  fvineqsneq  37405  pibt2  37410  wl-spae  37514  wl-aleq  37528  fin2so  37606  matunitlindf  37617  poimirlem4  37623  poimirlem26  37645  itg2addnclem  37670  upixp  37728  welb  37735  sdclem2  37741  metf1o  37754  sstotbnd3  37775  isbndx  37781  ismtycnv  37801  heiborlem4  37813  bfplem1  37821  opidonOLD  37851  grpomndo  37874  ax12eq  38939  ax12el  38940  cvrat4  39442  nn0addcom  42455  nn0mulcom  42459  mzpexpmpt  42738  diophren  42806  rmxypos  42940  jm2.17a  42953  jm2.17b  42954  rmygeid  42957  jm2.18  42981  jm2.25  42992  jm2.15nn0  42996  jm2.16nn0  42997  pwslnm  43087  isnumbasgrplem1  43094  dgraalem  43138  onuniintrab  43219  onsupuni  43222  onsupcl3  43226  naddonnn  43388  naddwordnexlem2  43391  relexpiidm  43697  relexpmulnn  43702  relexpmulg  43703  relexp01min  43706  relexp0a  43709  relexpxpmin  43710  clsk1indlem3  44036  grucollcld  44253  dvgrat  44305  radcnvrat  44307  sspwimpcf  44913  sspwimpcfVD  44914  e2ebindALT  44922  trfr  44956  et-sqrtnegnre  46874  fsetprcnexALT  47066  eu2ndop1stv  47129  afvfv0bi  47156  afveu  47157  afvres  47176  aovmpt4g  47205  ndmaovass  47210  ndmaovdistr  47211  afv2orxorb  47232  afv2eu  47242  imarnf1pr  47286  nltle2tri  47317  fzopredsuc  47327  subsubelfzo0  47330  2ffzoeq  47331  2tceilhalfelfzo1  47336  m1modmmod  47362  smonoord  47375  elsetpreimafvssdm  47390  iccpartres  47422  iccpartiltu  47426  iccpartigtl  47427  iccpartgt  47431  icceuelpartlem  47439  fargshiftf1  47445  ichnreuop  47476  ichreuopeq  47477  elsprel  47479  sprsymrelfo  47501  prproropf1olem4  47510  paireqne  47515  sbcpr  47525  reupr  47526  goldbachth  47551  fmtnoprmfac1  47569  fmtnoprmfac2  47571  prmdvdsfmtnof1lem2  47589  lighneallem2  47610  lighneallem4  47614  requad2  47627  even3prm2  47723  fpprwpprb  47744  gbegt5  47765  sbgoldbwt  47781  sbgoldbm  47788  nnsum3primesgbe  47796  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  bgoldbtbndlem2  47810  bgoldbtbndlem3  47811  bgoldbtbndlem4  47812  bgoldbtbnd  47813  isubgredg  47870  grimuhgr  47891  clnbgrgrim  47938  grtriprop  47945  cycl3grtrilem  47950  cycl3grtri  47951  gpgusgralem  48060  gpgedgvtx0  48065  gpgedgvtx1  48066  gpgcubic  48083  gpg5nbgr3star  48085  gpgprismgr4cycllem3  48101  upgrwlkupwlk  48144  uspgropssxp  48148  uspgrsprfo  48152  isassintop  48214  lidldomn1  48235  2zlidl  48244  2zrngamgm  48249  2zrngmmgm  48256  rngccatidALTV  48276  rngcinvALTV  48280  rhmsubcALTVlem4  48288  funcringcsetcALTV2lem9  48302  ringccatidALTV  48310  srhmsubcALTV  48329  lmodvsmdi  48383  ply1mulgsumlem1  48391  ply1mulgsumlem2  48392  lincdifsn  48429  lincsumcl  48436  lincscmcl  48437  lincext3  48461  lindslinindsimp1  48462  lindslinindsimp2lem5  48467  snlindsntor  48476  lincresunit2  48483  lincresunit3lem2  48485  zgtp1leeq  48526  elbigo2  48557  fllog2  48573  digexp  48612  dig1  48613  nn0sumshdiglemA  48624  nn0sumshdiglemB  48625  1arymaptf1  48647  2arymaptf1  48658  rrxlinec  48741  eenglngeehlnm  48744  rrx2linest  48747  itsclc0yqsol  48769  itsclc0xyqsol  48773