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  3305  gencl  3486  2gencl  3487  vtocl2ga  3541  vtocl2gaf  3542  vtocl3gaf  3544  vtocl3ga  3546  vtocl4g  3548  vtocl4ga  3549  rspccva  3584  2reurex  3728  2reu1  3857  rexdifi  4109  sseq0  4362  r19.2z  4454  ralf0  4473  falseral0  4475  elelpwi  4569  preqsnd  4819  prproe  4865  ssuni  4892  disji2  5086  disjiun  5090  disjxiun  5099  trintss  5228  ssexg  5273  reusv2lem3  5350  propeqop  5462  otiunsndisj  5475  rexopabb  5483  pofun  5557  solin  5566  2optocl  5726  3optocl  5727  ssrelrn  5848  elrnmpt1  5913  resieq  5950  imadifssran  6112  reuop  6254  fnun  6614  fss  6686  fun  6704  fvelimab  6915  fvmptss  6962  fvn0ssdmfun  7028  fvcofneq  7047  fmptco  7083  funsndifnop  7105  fnressn  7112  fressnfv  7114  fvn0fvelrnOLD  7117  fmptsng  7124  fvtp2g  7155  fvtp3g  7156  tpres  7157  fnex  7173  funfvima3  7192  fvf1pr  7264  isores3  7292  tfisg  7810  dmfex  7861  opreuopreu  7992  releldmdifi  8003  funeldmdif  8006  el2mpocsbcl  8041  f1o2ndf1  8078  frxp  8082  fnse  8089  frxp2  8100  frxp3  8107  poseq  8114  ressuppssdif  8141  funsssuppss  8146  mpoxopxnop0  8171  reldmtpos  8190  frrlem8  8249  fpr2a  8258  smores  8298  tfrlem7  8328  tz7.48-2  8387  tz7.49  8390  oacl  8476  omcl  8477  oecl  8478  oarec  8503  oewordri  8533  oeworde  8534  oelim2  8536  oeoa  8538  oeoelem  8539  oeoe  8540  nnacl  8552  nnmcl  8553  nnecl  8554  nnmsucr  8566  naddoa  8643  brinxper  8677  2ecoptocl  8758  fsetprcnex  8812  undifixp  8884  xpf1o  9080  limensuc  9095  unfi  9112  en1eqsn  9195  ac6sfi  9207  frfi  9208  difinf  9236  imafiOLD  9241  f1dmvrnfibi  9268  f1vrnfibi  9269  suppeqfsuppbi  9306  elfiun  9357  dffi3  9358  infsupprpr  9433  xpwdomg  9514  infdiffi  9587  ttrclselem2  9655  epfrs  9660  frmin  9678  frr2  9689  rankxpsuc  9811  updjud  9863  tskwe  9879  infxpenlem  9942  fseqenlem1  9953  kmlem2  10081  nnadju  10127  cff1  10187  cflim2  10192  sornom  10206  infpssrlem4  10235  fin23lem26  10254  fin23lem30  10271  fin23lem34  10275  isf32lem11  10292  fin67  10324  isfin7-2  10325  fin1a2lem10  10338  axcc2lem  10365  axdc2lem  10377  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  iunfo  10468  tsk0  10692  gruina  10747  grur1a  10748  mulcanenq  10889  reclem2pr  10977  supsrlem  11040  supsr  11041  ax1rid  11090  negf1o  11584  mulgt1OLD  12017  lbreu  12109  nnindd  12182  nnaddcl  12185  nnmulcl  12186  nn0n0n1ge2b  12487  nn0indd  12607  fzind  12608  fnn0ind  12609  uzaddcl  12839  uzinfi  12863  nn01to3  12876  elpq  12910  xmulasslem2  13218  supxrunb1  13255  supxrunb2  13256  infmremnf  13280  infmrp1  13281  uzsubsubfz  13483  fzdif1  13542  elfz0ubfz0  13569  fz0fzdiffz0  13574  elfzmlbp  13576  fzofzim  13646  elfzom1elp1fzo  13669  ssfzo12bi  13698  fzoopth  13699  fzonfzoufzol  13707  elfznelfzob  13710  injresinjlem  13724  injresinj  13725  modaddmodup  13875  modfzo0difsn  13884  modsumfzodifsn  13885  addmodlteq  13887  om2uzlti  13891  fsequb  13916  ssnn0fi  13926  ser1const  13999  expcllem  14013  expeq0  14033  expmordi  14108  expnngt1  14182  faclbnd  14231  hashf1rn  14293  hashgadd  14318  hashunx  14327  hashnn0n0nn  14332  hashgt0elex  14342  hashss  14350  hashfzp1  14372  hashxp  14375  hashmap  14376  hashimarni  14382  seqcoll  14405  hash2exprb  14412  hashge2el2difr  14422  elss2prb  14429  hashdifsnp1  14447  fi1uzind  14448  brfi1indALT  14451  lswlgt0cl  14510  swrdnd  14595  swrdnnn0nd  14597  swrdnd0  14598  swrd0  14599  swrdsbslen  14605  swrdspsleq  14606  pfxsuff1eqwrdeq  14640  swrdswrdlem  14645  swrdswrd  14646  wrd2ind  14664  pfxccatin12lem2a  14668  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12lem3  14673  pfxccatin12  14674  pfxccat3  14675  swrdccat  14676  pfxccat3a  14679  swrdccat3blem  14680  repswswrd  14725  repswrevw  14728  cshwmodn  14736  cshwsublen  14737  cshwidxmod  14744  cshwidxmodr  14745  cshf1  14751  2cshw  14754  cshweqrep  14762  cshw1  14763  2cshwcshw  14767  cshwcshid  14769  cshwcsh2id  14770  wrdlen2i  14884  2swrd2eqwrdeq  14895  wwlktovfo  14900  relexpsucnnl  14972  rtrclreclem3  15002  rtrclreclem4  15003  relexpindlem  15005  r19.29uz  15293  caubnd  15301  sqreu  15303  climshft  15518  climub  15604  climserle  15605  sumss  15666  sumss2  15668  modfsummods  15735  o1fsum  15755  binom  15772  climcndslem1  15791  climcndslem2  15792  cvgrat  15825  clim2prod  15830  prodfn0  15836  prodfrec  15837  ntrivcvgfvn0  15841  fprodn0  15921  fprodmodd  15939  fprodefsum  16037  demoivreALT  16145  ruclem8  16181  dvdsaddre2b  16253  dvdsdivcl  16262  dvdsfac  16272  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  m1exp1  16322  nn0o  16329  pwp1fsum  16337  flodddiv4  16361  smu01lem  16431  dvdslegcd  16450  gcdneg  16468  dfgcd2  16492  seq1st  16517  alginv  16521  lcmf  16579  lcmftp  16582  lcmfunsnlem2lem2  16585  lcmfunsnlem  16587  lcmfun  16591  ncoprmgcdne1b  16596  coprmproddvdslem  16608  coprmproddvds  16609  cncongr1  16613  prmdvdsexp  16661  prmndvdsfaclt  16671  ncoprmlnprm  16674  fvprmselgcd1  16992  prmgaplem6  17003  prmgaplem7  17004  prmgaplem8  17005  cshwshashlem1  17042  setsstruct2  17120  setsstruct  17122  inveq  17712  catsubcat  17777  initoeu2lem0  17951  initoeu2lem1  17952  funcestrcsetclem8  18084  funcestrcsetclem9  18085  fthestrcsetc  18087  fullestrcsetc  18088  funcsetcestrclem9  18100  fthsetcestrc  18102  fullsetcestrc  18103  lubss  18448  lubel  18449  mgmpropd  18554  issstrmgm  18556  mgmb1mgm1  18558  sgrpidmnd  18642  frmdgsum  18765  smndex1mndlem  18812  mgm2nsgrplem3  18823  dfgrp2  18870  cyccom  19111  gaass  19205  gsumwrev  19274  symgextf1lem  19326  symgextf1  19327  fvcosymgeq  19335  gsmsymgreq  19338  symgfixelsi  19341  pmtrprfv3  19360  symggen  19376  pmtrprfval  19393  gsumzres  19815  gsumpr  19861  gsumzunsnd  19862  srgmulgass  20102  srgbinom  20116  0ringnnzr  20410  rnghmsscmap  20515  rnghmsubcsetclem2  20517  rngcinv  20522  funcrngcsetc  20525  funcrngcsetcALT  20526  rhmsscmap  20544  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  funcringcsetc  20559  srhmsubc  20565  rhmsubclem4  20573  lmodvsmmulgdi  20779  lmodfopnelem1  20780  rmodislmodlem  20811  rngqiprngimfo  21187  cnfldmulg  21291  cnfldexp  21292  psgndiflemB  21485  assamulgscm  21786  gsumply1subr  22094  gsummoncoe1  22171  pf1ind  22218  matmulcell  22308  mat1dimscm  22338  dmatmul  22360  dmatscmcl  22366  scmataddcl  22379  scmatsubcl  22380  scmatsgrp1  22385  mavmulsolcl  22414  ma1repveval  22434  1marepvmarrepid  22438  symgmatr01lem  22516  slesolvec  22542  cramerimplem2  22547  decpmatmullem  22634  pm2mpf1  22662  mp2pm2mplem4  22672  monmat2matmon  22687  chpscmat  22705  chpscmatgsumbin  22707  fvmptnn04ifb  22714  chfacfscmul0  22721  chfacfscmulgsum  22723  chfacfpmmul0  22725  chfacfpmmulgsum  22727  cpmadugsumlemF  22739  toprntopon  22788  clsss  22917  ntrss  22918  restntr  23045  cmpsublem  23262  cmpsub  23263  2ndcrest  23317  txindislem  23496  t0kq  23681  filufint  23783  fbflim2  23840  flftg  23859  alexsubALTlem4  23913  cnextfvval  23928  ustuqtop4  24108  xmettri2  24204  mettri  24216  metss  24372  tngngp3  24520  clmvscom  24966  lmmbr  25134  caublcls  25185  lmcau  25189  ovolunlem1a  25373  nulmbl2  25413  voliunlem1  25427  iunmbl  25430  volsup  25433  dvlip  25874  dvfsumle  25902  dvfsumleOLD  25903  degltlem1  25953  ply1divex  26018  plyco  26122  dgrnznn  26128  dvnply2  26171  plydivex  26181  aannenlem2  26213  aaliou3lem2  26227  ulmcau  26280  zabsle1  27183  gausslemma2dlem1a  27252  gausslemma2dlem2  27254  gausslemma2dlem3  27255  gausslemma2dlem4  27256  2lgslem1a1  27276  2sqnn0  27325  2sqreulem1  27333  2sqreunnlem1  27336  dchrisumlem1  27376  dchrisumlem2  27377  dchrisumlem3  27378  qabvle  27512  ostthlem2  27515  ostth2lem2  27521  nosupbnd1lem5  27600  noinfbnd1lem5  27615  nocvxminlem  27665  nocvxmin  27666  slerec  27707  madebdaylemold  27785  mulsuniflem  28028  precsexlem6  28090  precsexlem7  28091  precsexlem8  28092  precsexlem9  28093  abssge0  28123  noseqind  28162  om2noseqlt  28169  om2noseqrdg  28174  n0addscl  28212  n0mulscl  28213  onsfi  28223  expscllem  28292  tgjustr  28377  axeuclidlem  28865  incistruhgr  28982  umgredgprv  29010  umgrpredgv  29043  usgredgprvALT  29098  uhgr2edg  29111  usgredg2vlem2  29129  lfuhgr1v0e  29157  subgrfun  29184  umgrres1lem  29213  upgrres1  29216  fusgrfis  29233  uhgrnbgr0nb  29257  nbgr1vtx  29261  nb3grprlem1  29283  uvtx01vtx  29300  fusgrn0degnn0  29403  vtxdginducedm1lem4  29446  finsumvtxdg2size  29454  wlkl1loop  29541  wlkres  29572  lfgrwlknloop  29591  pthdadjvtx  29631  dfpth2  29632  upgr2pthnlp  29635  upgrwlkdvdelem  29639  upgrwlkdvde  29640  uhgrwkspthlem2  29657  usgr2trlspth  29664  usgr2pth  29667  pthdlem2lem  29670  cyclnumvtx  29703  lfgrn1cycl  29708  uspgrn2crct  29711  crctcshwlkn0lem3  29715  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  iswspthsnon  29759  wlkiswwlks1  29770  wlklnwwlkln1  29771  wlkiswwlks2  29778  wlkiswwlksupgr2  29780  wlklnwwlkln2lem  29785  wlknwwlksnbij  29791  wwlksnred  29795  wwlksnext  29796  wwlksnredwwlkn  29798  wwlksnredwwlkn0  29799  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextsurj  29803  wspthsnonn0vne  29820  wspn0  29827  wwlks2onv  29856  elwwlks2  29869  elwspths2spth  29870  rusgrnumwwlk  29878  clwwlkccatlem  29891  clwlkclwwlklem2a1  29894  clwlkclwwlklem2fv2  29898  clwlkclwwlklem2a4  29899  clwlkclwwlklem2a  29900  clwlkclwwlklem2  29902  clwlkclwwlkf1lem3  29908  clwwisshclwwslem  29916  clwwisshclwwsn  29918  erclwwlktr  29924  isclwwlknx  29938  clwwlkinwwlk  29942  clwwlkel  29948  clwwlkf  29949  clwwlkf1  29951  clwwlkfo  29952  clwwlkext2edg  29958  wwlksext2clwwlk  29959  wwlksubclwwlk  29960  clwwlknscsh  29964  erclwwlkntr  29973  eleclclwwlkn  29978  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwwlknon0  29995  clwwlknonel  29997  clwwlknon1  29999  clwwlknonwwlknonb  30008  clwwlknonex2lem2  30010  clwwlknun  30014  clwwlkvbij  30015  upgr3v3e3cycl  30082  uhgr3cyclex  30084  upgr4cycl4dv4e  30087  eulerpath  30143  eucrctshift  30145  eucrct2eupth  30147  1to2vfriswmgr  30181  1to3vfriswmgr  30182  3cyclfrgrrn1  30187  4cycl2vnunb  30192  frgrwopreglem2  30215  frgrwopreglem3  30216  frgrwopreglem5ALT  30224  fusgr2wsp2nb  30236  2clwwlk2clwwlklem  30248  2clwwlk2clwwlk  30252  numclwwlk1lem2f1  30259  numclwwlk1lem2fo  30260  numclwwlk1  30263  clwwlknonclwlknonf1o  30264  dlwwlknondlwlknonf1o  30267  numclwlk1  30273  numclwlk2lem2f  30279  numclwlk2lem2f1o  30281  numclwwlk5  30290  frgrreg  30296  frgrregord013  30297  friendship  30301  nsnlplig  30383  nsnlpligALT  30384  isgrpo  30399  vcdi  30467  vcdir  30468  vcass  30469  nmosetre  30666  hlim2  31094  shscli  31219  chintcli  31233  dfch2  31309  spansncvi  31554  nmopsetretALT  31765  nmfnsetre  31779  lnopl  31816  lnfnl  31833  pjss2coi  32066  pjorthcoi  32071  pjscji  32072  pjssdif2i  32076  pjclem4a  32100  pj3lem1  32108  strlem5  32157  hstrlem5  32165  cvmdi  32226  mdslmd3i  32234  atcv1  32282  atcvat4i  32299  cdj3lem2a  32338  cdj3lem3a  32341  opreu2reuALT  32379  iuninc  32462  disji2f  32479  disjif2  32483  fmptcof2  32554  xrsmulgzz  32920  ofldchr  33265  1arithufdlem3  33490  esumfzf  34032  issgon  34086  voliune  34192  volfiniune  34193  rrvsum  34418  bnj228  34698  bnj1294  34780  bnj229  34847  bnj607  34879  bnj908  34894  bnj953  34902  bnj1118  34947  bnj1174  34966  bnj1388  34996  funen1cnv  35051  acycgrsubgr  35118  cvmliftlem15  35258  satfsschain  35324  satfdm  35329  satf0op  35337  fmla0xp  35343  gonarlem  35354  goalrlem  35356  satffunlem1lem1  35362  satffunlem2lem1  35364  dmopab3rexdif  35365  satefvfmla0  35378  prv1n  35391  iprodefisumlem  35700  faclimlem1  35703  dfon2lem6  35749  idinside  36045  onsucconni  36398  axc11n11r  36644  bj-brrelex12ALT  37028  bj-snmoore  37074  bj-finsumval0  37246  exlimim  37303  exellim  37305  icoreclin  37318  difunieq  37335  fvineqsneq  37373  pibt2  37378  wl-spae  37482  wl-aleq  37496  fin2so  37574  matunitlindf  37585  poimirlem4  37591  poimirlem26  37613  itg2addnclem  37638  upixp  37696  welb  37703  sdclem2  37709  metf1o  37722  sstotbnd3  37743  isbndx  37749  ismtycnv  37769  heiborlem4  37781  bfplem1  37789  opidonOLD  37819  grpomndo  37842  ax12eq  38907  ax12el  38908  cvrat4  39410  nn0addcom  42423  nn0mulcom  42427  mzpexpmpt  42706  diophren  42774  rmxypos  42909  jm2.17a  42922  jm2.17b  42923  rmygeid  42926  jm2.18  42950  jm2.25  42961  jm2.15nn0  42965  jm2.16nn0  42966  pwslnm  43056  isnumbasgrplem1  43063  dgraalem  43107  onuniintrab  43188  onsupuni  43191  onsupcl3  43195  naddonnn  43357  naddwordnexlem2  43360  relexpiidm  43666  relexpmulnn  43671  relexpmulg  43672  relexp01min  43675  relexp0a  43678  relexpxpmin  43679  clsk1indlem3  44005  grucollcld  44222  dvgrat  44274  radcnvrat  44276  sspwimpcf  44882  sspwimpcfVD  44883  e2ebindALT  44891  trfr  44925  et-sqrtnegnre  46844  fsetprcnexALT  47036  eu2ndop1stv  47099  afvfv0bi  47126  afveu  47127  afvres  47146  aovmpt4g  47175  ndmaovass  47180  ndmaovdistr  47181  afv2orxorb  47202  afv2eu  47212  imarnf1pr  47256  nltle2tri  47287  fzopredsuc  47297  subsubelfzo0  47300  2ffzoeq  47301  2tceilhalfelfzo1  47306  m1modmmod  47332  smonoord  47345  elsetpreimafvssdm  47360  iccpartres  47392  iccpartiltu  47396  iccpartigtl  47397  iccpartgt  47401  icceuelpartlem  47409  fargshiftf1  47415  ichnreuop  47446  ichreuopeq  47447  elsprel  47449  sprsymrelfo  47471  prproropf1olem4  47480  paireqne  47485  sbcpr  47495  reupr  47496  goldbachth  47521  fmtnoprmfac1  47539  fmtnoprmfac2  47541  prmdvdsfmtnof1lem2  47559  lighneallem2  47580  lighneallem4  47584  requad2  47597  even3prm2  47693  fpprwpprb  47714  gbegt5  47735  sbgoldbwt  47751  sbgoldbm  47758  nnsum3primesgbe  47766  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  bgoldbtbndlem2  47780  bgoldbtbndlem3  47781  bgoldbtbndlem4  47782  bgoldbtbnd  47783  isubgredg  47839  grimuhgr  47860  clnbgrgrim  47907  grtriprop  47913  cycl3grtrilem  47918  cycl3grtri  47919  gpgusgralem  48020  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgcubic  48043  gpg5nbgr3star  48045  gpgprismgr4cycllem3  48060  upgrwlkupwlk  48101  uspgropssxp  48105  uspgrsprfo  48109  isassintop  48171  lidldomn1  48192  2zlidl  48201  2zrngamgm  48206  2zrngmmgm  48213  rngccatidALTV  48233  rngcinvALTV  48237  rhmsubcALTVlem4  48245  funcringcsetcALTV2lem9  48259  ringccatidALTV  48267  srhmsubcALTV  48286  lmodvsmdi  48340  ply1mulgsumlem1  48348  ply1mulgsumlem2  48349  lincdifsn  48386  lincsumcl  48393  lincscmcl  48394  lincext3  48418  lindslinindsimp1  48419  lindslinindsimp2lem5  48424  snlindsntor  48433  lincresunit2  48440  lincresunit3lem2  48442  zgtp1leeq  48483  elbigo2  48514  fllog2  48530  digexp  48569  dig1  48570  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582  1arymaptf1  48604  2arymaptf1  48615  rrxlinec  48698  eenglngeehlnm  48701  rrx2linest  48704  itsclc0yqsol  48726  itsclc0xyqsol  48730