Theorem impcom 408

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpan9  511  bianir  1064  19.29r  1881  19.41v  1956  19.41  2247  nfsb4t  2507  mo4  2570  2euexv  2635  2euex  2645  gencl  3472  2gencl  3473  vtocl2ga  3521  vtocl2gaf  3522  vtocl3gaf  3523  vtocl3ga  3524  vtocl4g  3525  vtocl4ga  3526  rspccva  3559  2reurex  3701  2reu1  3829  rexdifi  4080  sseq0  4331  r19.2z  4427  falseral0OLD  4443  elelpwi  4539  preqsnd  4790  prproe  4836  ssuni  4863  disji2  5056  disjiun  5060  disjxiun  5069  trintss  5198  ssexg  5251  reusv2lem3  5329  propeqop  5448  otiunsndisj  5461  rexopabb  5470  pofun  5544  solin  5553  2optocl  5714  3optocl  5715  ssrelrn  5836  elrnmpt1  5902  resieq  5942  imadifssran  6102  reuop  6244  fnun  6599  fss  6671  fun  6689  fvelimab  6899  fvmptss  6948  fvn0ssdmfun  7015  fvcofneq  7034  fmptco  7071  funsndifnop  7094  fnressn  7101  fressnfv  7103  fmptsng  7112  fvtp2g  7143  fvtp3g  7144  tpres  7145  fnex  7161  funfvima3  7180  fvf1pr  7251  isores3  7279  tfisg  7794  dmfex  7845  opreuopreu  7976  releldmdifi  7987  funeldmdif  7990  el2mpocsbcl  8024  f1o2ndf1  8061  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  8518  oeworde  8519  oelim2  8521  oeoa  8523  oeoelem  8524  oeoe  8525  nnacl  8537  nnmcl  8538  nnecl  8539  nnmsucr  8551  naddoa  8628  brinxper  8663  2ecoptocl  8745  fsetprcnex  8799  undifixp  8872  xpf1o  9067  limensuc  9082  unfi  9095  en1eqsn  9175  ac6sfi  9184  frfi  9185  difinf  9211  imafiOLD  9216  f1dmvrnfibi  9241  f1vrnfibi  9242  suppeqfsuppbi  9282  elfiun  9333  dffi3  9334  infsupprpr  9409  xpwdomg  9490  infdiffi  9570  ttrclselem2  9638  epfrs  9643  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  10677  gruina  10732  grur1a  10733  mulcanenq  10874  reclem2pr  10962  supsrlem  11025  supsr  11026  ax1rid  11075  negf1o  11571  mulgt1OLD  12005  lbreu  12097  nnindd  12185  nnaddcl  12188  nnmulcl  12189  nn0n0n1ge2b  12497  nn0indd  12617  fzind  12618  fnn0ind  12619  uzaddcl  12845  uzinfi  12869  nn01to3  12882  elpq  12916  xmulasslem2  13225  supxrunb1  13262  supxrunb2  13263  infmremnf  13287  infmrp1  13288  uzsubsubfz  13491  fzdif1  13550  elfz0ubfz0  13577  fz0fzdiffz0  13582  elfzmlbp  13584  fzofzim  13655  elfzom1elp1fzo  13678  ssfzo12bi  13707  fzoopth  13708  fzonfzoufzol  13717  elfznelfzob  13720  injresinjlem  13736  injresinj  13737  modaddmodup  13887  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  om2uzlti  13903  fsequb  13928  ssnn0fi  13938  ser1const  14011  expcllem  14025  expeq0  14045  expmordi  14120  expnngt1  14194  faclbnd  14243  hashf1rn  14305  hashgadd  14330  hashunx  14339  hashnn0n0nn  14344  hashgt0elex  14354  hashss  14362  hashfzp1  14384  hashxp  14387  hashmap  14388  hashimarni  14394  seqcoll  14417  hash2exprb  14424  hashge2el2difr  14434  elss2prb  14441  hashdifsnp1  14459  fi1uzind  14460  brfi1indALT  14463  lswlgt0cl  14522  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  swrd0  14612  swrdsbslen  14618  swrdspsleq  14619  pfxsuff1eqwrdeq  14652  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  pfxccatin12  14686  pfxccat3  14687  swrdccat  14688  pfxccat3a  14691  swrdccat3blem  14692  repswswrd  14737  repswrevw  14740  cshwmodn  14748  cshwsublen  14749  cshwidxmod  14756  cshwidxmodr  14757  cshf1  14763  2cshw  14766  cshweqrep  14774  cshw1  14775  2cshwcshw  14778  cshwcshid  14780  cshwcsh2id  14781  wrdlen2i  14895  2swrd2eqwrdeq  14906  wwlktovfo  14911  relexpsucnnl  14983  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  r19.29uz  15304  caubnd  15312  sqreu  15314  climshft  15529  climub  15615  climserle  15616  sumss  15677  sumss2  15679  modfsummods  15747  o1fsum  15767  binom  15786  climcndslem1  15805  climcndslem2  15806  cvgrat  15839  clim2prod  15844  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  fprodn0  15935  fprodmodd  15953  fprodefsum  16051  demoivreALT  16159  ruclem8  16195  dvdsaddre2b  16267  dvdsdivcl  16276  dvdsfac  16286  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  m1exp1  16336  nn0o  16343  pwp1fsum  16351  flodddiv4  16375  smu01lem  16445  dvdslegcd  16464  gcdneg  16482  dfgcd2  16506  seq1st  16531  alginv  16535  lcmf  16593  lcmftp  16596  lcmfunsnlem2lem2  16599  lcmfunsnlem  16601  lcmfun  16605  ncoprmgcdne1b  16610  coprmproddvdslem  16622  coprmproddvds  16623  cncongr1  16627  prmdvdsexp  16676  prmndvdsfaclt  16686  ncoprmlnprm  16689  fvprmselgcd1  17007  prmgaplem6  17018  prmgaplem7  17019  prmgaplem8  17020  cshwshashlem1  17057  setsstruct2  17135  setsstruct  17137  inveq  17732  catsubcat  17797  initoeu2lem0  17971  initoeu2lem1  17972  funcestrcsetclem8  18104  funcestrcsetclem9  18105  fthestrcsetc  18107  fullestrcsetc  18108  funcsetcestrclem9  18120  fthsetcestrc  18122  fullsetcestrc  18123  lubss  18470  lubel  18471  mgmpropd  18610  issstrmgm  18612  mgmb1mgm1  18614  sgrpidmnd  18698  frmdgsum  18821  smndex1mndlem  18871  mgm2nsgrplem3  18882  dfgrp2  18929  cyccom  19169  gaass  19263  gsumwrev  19332  symgextf1lem  19386  symgextf1  19387  fvcosymgeq  19395  gsmsymgreq  19398  symgfixelsi  19401  pmtrprfv3  19420  symggen  19436  pmtrprfval  19453  gsumzres  19875  gsumpr  19921  gsumzunsnd  19922  srgmulgass  20189  srgbinom  20203  0ringnnzr  20497  rnghmsscmap  20602  rnghmsubcsetclem2  20604  rngcinv  20609  funcrngcsetc  20612  funcrngcsetcALT  20613  rhmsscmap  20631  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  funcringcsetc  20646  srhmsubc  20652  rhmsubclem4  20660  lmodvsmmulgdi  20887  lmodfopnelem1  20888  rmodislmodlem  20919  rngqiprngimfo  21294  cnfldmulg  21379  cnfldexp  21380  ofldchr  21551  psgndiflemB  21575  assamulgscm  21876  gsumply1subr  22218  gsummoncoe1  22294  pf1ind  22341  matmulcell  22428  mat1dimscm  22458  dmatmul  22480  dmatscmcl  22486  scmataddcl  22499  scmatsubcl  22500  scmatsgrp1  22505  mavmulsolcl  22534  ma1repveval  22554  1marepvmarrepid  22558  symgmatr01lem  22636  slesolvec  22662  cramerimplem2  22667  decpmatmullem  22754  pm2mpf1  22782  mp2pm2mplem4  22792  monmat2matmon  22807  chpscmat  22825  chpscmatgsumbin  22827  fvmptnn04ifb  22834  chfacfscmul0  22841  chfacfscmulgsum  22843  chfacfpmmul0  22845  chfacfpmmulgsum  22847  cpmadugsumlemF  22859  toprntopon  22908  clsss  23037  ntrss  23038  restntr  23165  cmpsublem  23382  cmpsub  23383  2ndcrest  23437  txindislem  23616  t0kq  23801  filufint  23903  fbflim2  23960  flftg  23979  alexsubALTlem4  24033  cnextfvval  24048  ustuqtop4  24227  xmettri2  24323  mettri  24335  metss  24491  tngngp3  24639  clmvscom  25075  lmmbr  25243  caublcls  25294  lmcau  25298  ovolunlem1a  25481  nulmbl2  25521  voliunlem1  25535  iunmbl  25538  volsup  25541  dvlip  25978  dvfsumle  26006  degltlem1  26055  ply1divex  26120  plyco  26224  dgrnznn  26230  dvnply2  26271  plydivex  26281  aannenlem2  26313  aaliou3lem2  26327  ulmcau  26378  zabsle1  27277  gausslemma2dlem1a  27346  gausslemma2dlem2  27348  gausslemma2dlem3  27349  gausslemma2dlem4  27350  2lgslem1a1  27370  2sqnn0  27419  2sqreulem1  27427  2sqreunnlem1  27430  dchrisumlem1  27470  dchrisumlem2  27471  dchrisumlem3  27472  qabvle  27606  ostthlem2  27609  ostth2lem2  27615  nosupbnd1lem5  27694  noinfbnd1lem5  27709  nocvxminlem  27764  lesrec  27809  madebdaylemold  27908  mulsuniflem  28159  precsexlem6  28222  precsexlem7  28223  precsexlem8  28224  precsexlem9  28225  abssge0  28255  noseqind  28302  om2noseqlt  28309  om2noseqrdg  28314  n0addscl  28354  n0mulscl  28355  onsfi  28366  oldfib  28387  expscllem  28440  pw2cut2  28472  z12zsodd  28492  tgjustr  28560  axeuclidlem  29049  incistruhgr  29166  umgredgprv  29194  umgrpredgv  29227  usgredgprvALT  29282  uhgr2edg  29295  usgredg2vlem2  29313  lfuhgr1v0e  29341  subgrfun  29368  umgrres1lem  29397  upgrres1  29400  fusgrfis  29417  uhgrnbgr0nb  29441  nbgr1vtx  29445  nb3grprlem1  29467  uvtx01vtx  29484  fusgrn0degnn0  29586  vtxdginducedm1lem4  29629  finsumvtxdg2size  29637  wlkl1loop  29724  wlkres  29755  lfgrwlknloop  29774  pthdadjvtx  29814  dfpth2  29815  upgr2pthnlp  29818  upgrwlkdvdelem  29822  upgrwlkdvde  29823  uhgrwkspthlem2  29840  usgr2trlspth  29847  usgr2pth  29850  pthdlem2lem  29853  cyclnumvtx  29886  lfgrn1cycl  29891  uspgrn2crct  29894  crctcshwlkn0lem3  29898  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  iswspthsnon  29942  wlkiswwlks1  29953  wlklnwwlkln1  29954  wlkiswwlks2  29961  wlkiswwlksupgr2  29963  wlklnwwlkln2lem  29968  wlknwwlksnbij  29974  wwlksnred  29978  wwlksnext  29979  wwlksnredwwlkn  29981  wwlksnredwwlkn0  29982  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextsurj  29986  wspthsnonn0vne  30003  wspn0  30010  wwlks2onv  30039  elwwlks2  30055  elwspths2spth  30056  rusgrnumwwlk  30064  clwwlkccatlem  30077  clwlkclwwlklem2a1  30080  clwlkclwwlklem2fv2  30084  clwlkclwwlklem2a4  30085  clwlkclwwlklem2a  30086  clwlkclwwlklem2  30088  clwlkclwwlkf1lem3  30094  clwwisshclwwslem  30102  clwwisshclwwsn  30104  erclwwlktr  30110  isclwwlknx  30124  clwwlkinwwlk  30128  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  clwwlkfo  30138  clwwlkext2edg  30144  wwlksext2clwwlk  30145  wwlksubclwwlk  30146  clwwlknscsh  30150  erclwwlkntr  30159  eleclclwwlkn  30164  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  clwwlknon0  30181  clwwlknonel  30183  clwwlknon1  30185  clwwlknonwwlknonb  30194  clwwlknonex2lem2  30196  clwwlknun  30200  clwwlkvbij  30201  upgr3v3e3cycl  30268  uhgr3cyclex  30270  upgr4cycl4dv4e  30273  eulerpath  30329  eucrctshift  30331  eucrct2eupth  30333  1to2vfriswmgr  30367  1to3vfriswmgr  30368  3cyclfrgrrn1  30373  4cycl2vnunb  30378  frgrwopreglem2  30401  frgrwopreglem3  30402  frgrwopreglem5ALT  30410  fusgr2wsp2nb  30422  2clwwlk2clwwlklem  30434  2clwwlk2clwwlk  30438  numclwwlk1lem2f1  30445  numclwwlk1lem2fo  30446  numclwwlk1  30449  clwwlknonclwlknonf1o  30450  dlwwlknondlwlknonf1o  30453  numclwlk1  30459  numclwlk2lem2f  30465  numclwlk2lem2f1o  30467  numclwwlk5  30476  frgrreg  30482  frgrregord013  30483  friendship  30487  nsnlplig  30570  nsnlpligALT  30571  isgrpo  30586  vcdi  30654  vcdir  30655  vcass  30656  nmosetre  30853  hlim2  31281  shscli  31406  chintcli  31420  dfch2  31496  spansncvi  31741  nmopsetretALT  31952  nmfnsetre  31966  lnopl  32003  lnfnl  32020  pjss2coi  32253  pjorthcoi  32258  pjscji  32259  pjssdif2i  32263  pjclem4a  32287  pj3lem1  32295  strlem5  32344  hstrlem5  32352  cvmdi  32413  mdslmd3i  32421  atcv1  32469  atcvat4i  32486  cdj3lem2a  32525  cdj3lem3a  32528  opreu2reuALT  32564  iuninc  32649  disji2f  32666  disjif2  32670  fmptcof2  32749  xrsmulgzz  33088  1arithufdlem3  33629  esumfzf  34253  issgon  34307  voliune  34413  volfiniune  34414  rrvsum  34638  bnj228  34918  bnj1294  34999  bnj229  35066  bnj607  35098  bnj908  35113  bnj953  35121  bnj1118  35166  bnj1174  35185  bnj1388  35215  funen1cnv  35269  rankfilimbi  35282  r1filimi  35284  trssfir1om  35292  trssfir1omregs  35317  acycgrsubgr  35386  cvmliftlem15  35526  satfsschain  35592  satfdm  35597  satf0op  35605  fmla0xp  35611  gonarlem  35622  goalrlem  35624  satffunlem1lem1  35630  satffunlem2lem1  35632  dmopab3rexdif  35633  satefvfmla0  35646  prv1n  35659  iprodefisumlem  35968  faclimlem1  35971  dfon2lem6  36014  idinside  36312  onsucconni  36665  axuntco  36707  ttcmin  36724  elttctr  36733  dfttc2g  36734  mh-inf3f1  36769  bj-cbvew  36982  axc11n11r  37026  bj-brrelex12ALT  37420  bj-snmoore  37471  bj-finsumval0  37645  exlimim  37704  exellim  37706  icoreclin  37719  difunieq  37736  fvineqsneq  37774  pibt2  37779  wl-spae  37892  wl-aleq  37906  fin2so  37974  matunitlindf  37985  poimirlem4  37991  poimirlem26  38013  itg2addnclem  38038  upixp  38096  welb  38103  sdclem2  38109  metf1o  38122  sstotbnd3  38143  isbndx  38149  ismtycnv  38169  heiborlem4  38181  bfplem1  38189  opidonOLD  38219  grpomndo  38242  eldisjdmqsim2  39183  ax12eq  39433  ax12el  39434  cvrat4  39935  nn0addcom  42952  nn0mulcom  42956  mzpexpmpt  43194  diophren  43258  rmxypos  43392  jm2.17a  43405  jm2.17b  43406  rmygeid  43409  jm2.18  43433  jm2.25  43444  jm2.15nn0  43448  jm2.16nn0  43449  pwslnm  43539  isnumbasgrplem1  43546  dgraalem  43590  onuniintrab  43671  onsupuni  43674  onsupcl3  43678  naddonnn  43840  naddwordnexlem2  43843  relexpiidm  44148  relexpmulnn  44153  relexpmulg  44154  relexp01min  44157  relexp0a  44160  relexpxpmin  44161  clsk1indlem3  44487  grucollcld  44704  dvgrat  44756  radcnvrat  44758  sspwimpcf  45363  sspwimpcfVD  45364  e2ebindALT  45372  trfr  45406  et-sqrtnegnre  47316  fsetprcnexALT  47525  eu2ndop1stv  47588  afvfv0bi  47615  afveu  47616  afvres  47635  aovmpt4g  47664  ndmaovass  47669  ndmaovdistr  47670  afv2orxorb  47691  afv2eu  47701  imarnf1pr  47745  nltle2tri  47776  fzopredsuc  47787  subsubelfzo0  47790  2ffzoeq  47791  2tceilhalfelfzo1  47799  m1modmmod  47827  smonoord  47840  elsetpreimafvssdm  47861  iccpartres  47893  iccpartiltu  47897  iccpartigtl  47898  iccpartgt  47902  icceuelpartlem  47910  fargshiftf1  47916  ichnreuop  47947  ichreuopeq  47948  elsprel  47950  sprsymrelfo  47972  prproropf1olem4  47981  paireqne  47986  sbcpr  47996  reupr  47997  goldbachth  48025  fmtnoprmfac1  48043  fmtnoprmfac2  48045  prmdvdsfmtnof1lem2  48063  lighneallem2  48084  lighneallem4  48088  requad2  48114  even3prm2  48210  fpprwpprb  48231  gbegt5  48252  sbgoldbwt  48268  sbgoldbm  48275  nnsum3primesgbe  48283  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbndlem4  48299  bgoldbtbnd  48300  isubgredg  48357  grimuhgr  48378  clnbgrgrim  48425  grtriprop  48432  cycl3grtrilem  48437  cycl3grtri  48438  gpgusgralem  48547  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgcubic  48570  gpg5nbgr3star  48572  gpgprismgr4cycllem3  48588  upgrwlkupwlk  48631  uspgropssxp  48635  uspgrsprfo  48639  isassintop  48701  lidldomn1  48722  2zlidl  48731  2zrngamgm  48736  2zrngmmgm  48743  rngccatidALTV  48763  rngcinvALTV  48767  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem9  48789  ringccatidALTV  48797  srhmsubcALTV  48816  lmodvsmdi  48870  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  lincdifsn  48915  lincsumcl  48922  lincscmcl  48923  lincext3  48947  lindslinindsimp1  48948  lindslinindsimp2lem5  48953  snlindsntor  48962  lincresunit2  48969  lincresunit3lem2  48971  zgtp1leeq  49012  elbigo2  49043  fllog2  49059  digexp  49098  dig1  49099  nn0sumshdiglemA  49110  nn0sumshdiglemB  49111  1arymaptf1  49133  2arymaptf1  49144  rrxlinec  49227  eenglngeehlnm  49230  rrx2linest  49233  itsclc0yqsol  49255  itsclc0xyqsol  49259