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  2238  nfsb4t  2499  mo4  2561  2euexv  2626  2euex  2636  raleqbidvvOLD  3301  gencl  3478  2gencl  3479  vtocl2ga  3529  vtocl2gaf  3530  vtocl3gaf  3532  vtocl3ga  3534  vtocl4g  3536  vtocl4ga  3537  rspccva  3571  2reurex  3714  2reu1  3843  rexdifi  4095  sseq0  4348  r19.2z  4440  ralf0  4459  falseral0  4461  elelpwi  4555  preqsnd  4806  prproe  4852  ssuni  4879  disji2  5070  disjiun  5074  disjxiun  5083  trintss  5211  ssexg  5256  reusv2lem3  5333  propeqop  5442  otiunsndisj  5455  rexopabb  5463  pofun  5537  solin  5546  2optocl  5707  3optocl  5708  ssrelrn  5829  elrnmpt1  5895  resieq  5934  imadifssran  6093  reuop  6235  fnun  6590  fss  6662  fun  6680  fvelimab  6889  fvmptss  6936  fvn0ssdmfun  7002  fvcofneq  7021  fmptco  7057  funsndifnop  7079  fnressn  7086  fressnfv  7088  fmptsng  7097  fvtp2g  7128  fvtp3g  7129  tpres  7130  fnex  7146  funfvima3  7165  fvf1pr  7236  isores3  7264  tfisg  7779  dmfex  7830  opreuopreu  7961  releldmdifi  7972  funeldmdif  7975  el2mpocsbcl  8010  f1o2ndf1  8047  frxp  8051  fnse  8058  frxp2  8069  frxp3  8076  poseq  8083  ressuppssdif  8110  funsssuppss  8115  mpoxopxnop0  8140  reldmtpos  8159  frrlem8  8218  fpr2a  8227  smores  8267  tfrlem7  8297  tz7.48-2  8356  tz7.49  8359  oacl  8445  omcl  8446  oecl  8447  oarec  8472  oewordri  8502  oeworde  8503  oelim2  8505  oeoa  8507  oeoelem  8508  oeoe  8509  nnacl  8521  nnmcl  8522  nnecl  8523  nnmsucr  8535  naddoa  8612  brinxper  8646  2ecoptocl  8727  fsetprcnex  8781  undifixp  8853  xpf1o  9047  limensuc  9062  unfi  9075  en1eqsn  9154  ac6sfi  9163  frfi  9164  difinf  9190  imafiOLD  9195  f1dmvrnfibi  9220  f1vrnfibi  9221  suppeqfsuppbi  9258  elfiun  9309  dffi3  9310  infsupprpr  9385  xpwdomg  9466  infdiffi  9543  ttrclselem2  9611  epfrs  9616  frmin  9637  frr2  9648  rankxpsuc  9770  updjud  9822  tskwe  9838  infxpenlem  9899  fseqenlem1  9910  kmlem2  10038  nnadju  10084  cff1  10144  cflim2  10149  sornom  10163  infpssrlem4  10192  fin23lem26  10211  fin23lem30  10228  fin23lem34  10232  isf32lem11  10249  fin67  10281  isfin7-2  10282  fin1a2lem10  10295  axcc2lem  10322  axdc2lem  10334  axdc3lem2  10337  axdc3lem4  10339  axdc4lem  10341  iunfo  10425  tsk0  10649  gruina  10704  grur1a  10705  mulcanenq  10846  reclem2pr  10934  supsrlem  10997  supsr  10998  ax1rid  11047  negf1o  11542  mulgt1OLD  11975  lbreu  12067  nnindd  12140  nnaddcl  12143  nnmulcl  12144  nn0n0n1ge2b  12445  nn0indd  12565  fzind  12566  fnn0ind  12567  uzaddcl  12797  uzinfi  12821  nn01to3  12834  elpq  12868  xmulasslem2  13176  supxrunb1  13213  supxrunb2  13214  infmremnf  13238  infmrp1  13239  uzsubsubfz  13441  fzdif1  13500  elfz0ubfz0  13527  fz0fzdiffz0  13532  elfzmlbp  13534  fzofzim  13604  elfzom1elp1fzo  13627  ssfzo12bi  13656  fzoopth  13657  fzonfzoufzol  13666  elfznelfzob  13669  injresinjlem  13685  injresinj  13686  modaddmodup  13836  modfzo0difsn  13845  modsumfzodifsn  13846  addmodlteq  13848  om2uzlti  13852  fsequb  13877  ssnn0fi  13887  ser1const  13960  expcllem  13974  expeq0  13994  expmordi  14069  expnngt1  14143  faclbnd  14192  hashf1rn  14254  hashgadd  14279  hashunx  14288  hashnn0n0nn  14293  hashgt0elex  14303  hashss  14311  hashfzp1  14333  hashxp  14336  hashmap  14337  hashimarni  14343  seqcoll  14366  hash2exprb  14373  hashge2el2difr  14383  elss2prb  14390  hashdifsnp1  14408  fi1uzind  14409  brfi1indALT  14412  lswlgt0cl  14471  swrdnd  14557  swrdnnn0nd  14559  swrdnd0  14560  swrd0  14561  swrdsbslen  14567  swrdspsleq  14568  pfxsuff1eqwrdeq  14601  swrdswrdlem  14606  swrdswrd  14607  wrd2ind  14625  pfxccatin12lem2a  14629  swrdccatin2  14631  pfxccatin12lem2  14633  pfxccatin12lem3  14634  pfxccatin12  14635  pfxccat3  14636  swrdccat  14637  pfxccat3a  14640  swrdccat3blem  14641  repswswrd  14686  repswrevw  14689  cshwmodn  14697  cshwsublen  14698  cshwidxmod  14705  cshwidxmodr  14706  cshf1  14712  2cshw  14715  cshweqrep  14723  cshw1  14724  2cshwcshw  14727  cshwcshid  14729  cshwcsh2id  14730  wrdlen2i  14844  2swrd2eqwrdeq  14855  wwlktovfo  14860  relexpsucnnl  14932  rtrclreclem3  14962  rtrclreclem4  14963  relexpindlem  14965  r19.29uz  15253  caubnd  15261  sqreu  15263  climshft  15478  climub  15564  climserle  15565  sumss  15626  sumss2  15628  modfsummods  15695  o1fsum  15715  binom  15732  climcndslem1  15751  climcndslem2  15752  cvgrat  15785  clim2prod  15790  prodfn0  15796  prodfrec  15797  ntrivcvgfvn0  15801  fprodn0  15881  fprodmodd  15899  fprodefsum  15997  demoivreALT  16105  ruclem8  16141  dvdsaddre2b  16213  dvdsdivcl  16222  dvdsfac  16232  oddnn02np1  16254  oddge22np1  16255  evennn02n  16256  evennn2n  16257  m1exp1  16282  nn0o  16289  pwp1fsum  16297  flodddiv4  16321  smu01lem  16391  dvdslegcd  16410  gcdneg  16428  dfgcd2  16452  seq1st  16477  alginv  16481  lcmf  16539  lcmftp  16542  lcmfunsnlem2lem2  16545  lcmfunsnlem  16547  lcmfun  16551  ncoprmgcdne1b  16556  coprmproddvdslem  16568  coprmproddvds  16569  cncongr1  16573  prmdvdsexp  16621  prmndvdsfaclt  16631  ncoprmlnprm  16634  fvprmselgcd1  16952  prmgaplem6  16963  prmgaplem7  16964  prmgaplem8  16965  cshwshashlem1  17002  setsstruct2  17080  setsstruct  17082  inveq  17676  catsubcat  17741  initoeu2lem0  17915  initoeu2lem1  17916  funcestrcsetclem8  18048  funcestrcsetclem9  18049  fthestrcsetc  18051  fullestrcsetc  18052  funcsetcestrclem9  18064  fthsetcestrc  18066  fullsetcestrc  18067  lubss  18414  lubel  18415  mgmpropd  18554  issstrmgm  18556  mgmb1mgm1  18558  sgrpidmnd  18642  frmdgsum  18765  smndex1mndlem  18812  mgm2nsgrplem3  18823  dfgrp2  18870  cyccom  19110  gaass  19204  gsumwrev  19273  symgextf1lem  19327  symgextf1  19328  fvcosymgeq  19336  gsmsymgreq  19339  symgfixelsi  19342  pmtrprfv3  19361  symggen  19377  pmtrprfval  19394  gsumzres  19816  gsumpr  19862  gsumzunsnd  19863  srgmulgass  20130  srgbinom  20144  0ringnnzr  20435  rnghmsscmap  20540  rnghmsubcsetclem2  20542  rngcinv  20547  funcrngcsetc  20550  funcrngcsetcALT  20551  rhmsscmap  20569  rhmsubcsetclem2  20571  rhmsubcrngclem2  20577  funcringcsetc  20584  srhmsubc  20590  rhmsubclem4  20598  lmodvsmmulgdi  20825  lmodfopnelem1  20826  rmodislmodlem  20857  rngqiprngimfo  21233  cnfldmulg  21335  cnfldexp  21336  ofldchr  21508  psgndiflemB  21532  assamulgscm  21833  gsumply1subr  22141  gsummoncoe1  22218  pf1ind  22265  matmulcell  22355  mat1dimscm  22385  dmatmul  22407  dmatscmcl  22413  scmataddcl  22426  scmatsubcl  22427  scmatsgrp1  22432  mavmulsolcl  22461  ma1repveval  22481  1marepvmarrepid  22485  symgmatr01lem  22563  slesolvec  22589  cramerimplem2  22594  decpmatmullem  22681  pm2mpf1  22709  mp2pm2mplem4  22719  monmat2matmon  22734  chpscmat  22752  chpscmatgsumbin  22754  fvmptnn04ifb  22761  chfacfscmul0  22768  chfacfscmulgsum  22770  chfacfpmmul0  22772  chfacfpmmulgsum  22774  cpmadugsumlemF  22786  toprntopon  22835  clsss  22964  ntrss  22965  restntr  23092  cmpsublem  23309  cmpsub  23310  2ndcrest  23364  txindislem  23543  t0kq  23728  filufint  23830  fbflim2  23887  flftg  23906  alexsubALTlem4  23960  cnextfvval  23975  ustuqtop4  24154  xmettri2  24250  mettri  24262  metss  24418  tngngp3  24566  clmvscom  25012  lmmbr  25180  caublcls  25231  lmcau  25235  ovolunlem1a  25419  nulmbl2  25459  voliunlem1  25473  iunmbl  25476  volsup  25479  dvlip  25920  dvfsumle  25948  dvfsumleOLD  25949  degltlem1  25999  ply1divex  26064  plyco  26168  dgrnznn  26174  dvnply2  26217  plydivex  26227  aannenlem2  26259  aaliou3lem2  26273  ulmcau  26326  zabsle1  27229  gausslemma2dlem1a  27298  gausslemma2dlem2  27300  gausslemma2dlem3  27301  gausslemma2dlem4  27302  2lgslem1a1  27322  2sqnn0  27371  2sqreulem1  27379  2sqreunnlem1  27382  dchrisumlem1  27422  dchrisumlem2  27423  dchrisumlem3  27424  qabvle  27558  ostthlem2  27561  ostth2lem2  27567  nosupbnd1lem5  27646  noinfbnd1lem5  27661  nocvxminlem  27712  slerec  27755  madebdaylemold  27838  mulsuniflem  28083  precsexlem6  28145  precsexlem7  28146  precsexlem8  28147  precsexlem9  28148  abssge0  28178  noseqind  28217  om2noseqlt  28224  om2noseqrdg  28229  n0addscl  28267  n0mulscl  28268  onsfi  28278  expscllem  28348  pw2cut2  28377  zs12zodd  28387  tgjustr  28447  axeuclidlem  28935  incistruhgr  29052  umgredgprv  29080  umgrpredgv  29113  usgredgprvALT  29168  uhgr2edg  29181  usgredg2vlem2  29199  lfuhgr1v0e  29227  subgrfun  29254  umgrres1lem  29283  upgrres1  29286  fusgrfis  29303  uhgrnbgr0nb  29327  nbgr1vtx  29331  nb3grprlem1  29353  uvtx01vtx  29370  fusgrn0degnn0  29473  vtxdginducedm1lem4  29516  finsumvtxdg2size  29524  wlkl1loop  29611  wlkres  29642  lfgrwlknloop  29661  pthdadjvtx  29701  dfpth2  29702  upgr2pthnlp  29705  upgrwlkdvdelem  29709  upgrwlkdvde  29710  uhgrwkspthlem2  29727  usgr2trlspth  29734  usgr2pth  29737  pthdlem2lem  29740  cyclnumvtx  29773  lfgrn1cycl  29778  uspgrn2crct  29781  crctcshwlkn0lem3  29785  crctcshwlkn0lem4  29786  crctcshwlkn0lem5  29787  iswspthsnon  29829  wlkiswwlks1  29840  wlklnwwlkln1  29841  wlkiswwlks2  29848  wlkiswwlksupgr2  29850  wlklnwwlkln2lem  29855  wlknwwlksnbij  29861  wwlksnred  29865  wwlksnext  29866  wwlksnredwwlkn  29868  wwlksnredwwlkn0  29869  wwlksnextfun  29871  wwlksnextinj  29872  wwlksnextsurj  29873  wspthsnonn0vne  29890  wspn0  29897  wwlks2onv  29926  elwwlks2  29939  elwspths2spth  29940  rusgrnumwwlk  29948  clwwlkccatlem  29961  clwlkclwwlklem2a1  29964  clwlkclwwlklem2fv2  29968  clwlkclwwlklem2a4  29969  clwlkclwwlklem2a  29970  clwlkclwwlklem2  29972  clwlkclwwlkf1lem3  29978  clwwisshclwwslem  29986  clwwisshclwwsn  29988  erclwwlktr  29994  isclwwlknx  30008  clwwlkinwwlk  30012  clwwlkel  30018  clwwlkf  30019  clwwlkf1  30021  clwwlkfo  30022  clwwlkext2edg  30028  wwlksext2clwwlk  30029  wwlksubclwwlk  30030  clwwlknscsh  30034  erclwwlkntr  30043  eleclclwwlkn  30048  hashecclwwlkn1  30049  umgrhashecclwwlk  30050  clwwlknon0  30065  clwwlknonel  30067  clwwlknon1  30069  clwwlknonwwlknonb  30078  clwwlknonex2lem2  30080  clwwlknun  30084  clwwlkvbij  30085  upgr3v3e3cycl  30152  uhgr3cyclex  30154  upgr4cycl4dv4e  30157  eulerpath  30213  eucrctshift  30215  eucrct2eupth  30217  1to2vfriswmgr  30251  1to3vfriswmgr  30252  3cyclfrgrrn1  30257  4cycl2vnunb  30262  frgrwopreglem2  30285  frgrwopreglem3  30286  frgrwopreglem5ALT  30294  fusgr2wsp2nb  30306  2clwwlk2clwwlklem  30318  2clwwlk2clwwlk  30322  numclwwlk1lem2f1  30329  numclwwlk1lem2fo  30330  numclwwlk1  30333  clwwlknonclwlknonf1o  30334  dlwwlknondlwlknonf1o  30337  numclwlk1  30343  numclwlk2lem2f  30349  numclwlk2lem2f1o  30351  numclwwlk5  30360  frgrreg  30366  frgrregord013  30367  friendship  30371  nsnlplig  30453  nsnlpligALT  30454  isgrpo  30469  vcdi  30537  vcdir  30538  vcass  30539  nmosetre  30736  hlim2  31164  shscli  31289  chintcli  31303  dfch2  31379  spansncvi  31624  nmopsetretALT  31835  nmfnsetre  31849  lnopl  31886  lnfnl  31903  pjss2coi  32136  pjorthcoi  32141  pjscji  32142  pjssdif2i  32146  pjclem4a  32170  pj3lem1  32178  strlem5  32227  hstrlem5  32235  cvmdi  32296  mdslmd3i  32304  atcv1  32352  atcvat4i  32369  cdj3lem2a  32408  cdj3lem3a  32411  opreu2reuALT  32448  iuninc  32532  disji2f  32549  disjif2  32553  fmptcof2  32631  xrsmulgzz  32982  1arithufdlem3  33503  esumfzf  34074  issgon  34128  voliune  34234  volfiniune  34235  rrvsum  34459  bnj228  34739  bnj1294  34821  bnj229  34888  bnj607  34920  bnj908  34935  bnj953  34943  bnj1118  34988  bnj1174  35007  bnj1388  35037  funen1cnv  35092  rankfilimbi  35104  r1filimi  35106  trssfir1om  35114  trssfir1omregs  35124  acycgrsubgr  35194  cvmliftlem15  35334  satfsschain  35400  satfdm  35405  satf0op  35413  fmla0xp  35419  gonarlem  35430  goalrlem  35432  satffunlem1lem1  35438  satffunlem2lem1  35440  dmopab3rexdif  35441  satefvfmla0  35454  prv1n  35467  iprodefisumlem  35776  faclimlem1  35779  dfon2lem6  35822  idinside  36118  onsucconni  36471  axc11n11r  36717  bj-brrelex12ALT  37101  bj-snmoore  37147  bj-finsumval0  37319  exlimim  37376  exellim  37378  icoreclin  37391  difunieq  37408  fvineqsneq  37446  pibt2  37451  wl-spae  37555  wl-aleq  37569  fin2so  37647  matunitlindf  37658  poimirlem4  37664  poimirlem26  37686  itg2addnclem  37711  upixp  37769  welb  37776  sdclem2  37782  metf1o  37795  sstotbnd3  37816  isbndx  37822  ismtycnv  37842  heiborlem4  37854  bfplem1  37862  opidonOLD  37892  grpomndo  37915  ax12eq  38980  ax12el  38981  cvrat4  39482  nn0addcom  42495  nn0mulcom  42499  mzpexpmpt  42778  diophren  42846  rmxypos  42980  jm2.17a  42993  jm2.17b  42994  rmygeid  42997  jm2.18  43021  jm2.25  43032  jm2.15nn0  43036  jm2.16nn0  43037  pwslnm  43127  isnumbasgrplem1  43134  dgraalem  43178  onuniintrab  43259  onsupuni  43262  onsupcl3  43266  naddonnn  43428  naddwordnexlem2  43431  relexpiidm  43737  relexpmulnn  43742  relexpmulg  43743  relexp01min  43746  relexp0a  43749  relexpxpmin  43750  clsk1indlem3  44076  grucollcld  44293  dvgrat  44345  radcnvrat  44347  sspwimpcf  44952  sspwimpcfVD  44953  e2ebindALT  44961  trfr  44995  et-sqrtnegnre  46911  fsetprcnexALT  47093  eu2ndop1stv  47156  afvfv0bi  47183  afveu  47184  afvres  47203  aovmpt4g  47232  ndmaovass  47237  ndmaovdistr  47238  afv2orxorb  47259  afv2eu  47269  imarnf1pr  47313  nltle2tri  47344  fzopredsuc  47354  subsubelfzo0  47357  2ffzoeq  47358  2tceilhalfelfzo1  47363  m1modmmod  47389  smonoord  47402  elsetpreimafvssdm  47417  iccpartres  47449  iccpartiltu  47453  iccpartigtl  47454  iccpartgt  47458  icceuelpartlem  47466  fargshiftf1  47472  ichnreuop  47503  ichreuopeq  47504  elsprel  47506  sprsymrelfo  47528  prproropf1olem4  47537  paireqne  47542  sbcpr  47552  reupr  47553  goldbachth  47578  fmtnoprmfac1  47596  fmtnoprmfac2  47598  prmdvdsfmtnof1lem2  47616  lighneallem2  47637  lighneallem4  47641  requad2  47654  even3prm2  47750  fpprwpprb  47771  gbegt5  47792  sbgoldbwt  47808  sbgoldbm  47815  nnsum3primesgbe  47823  wtgoldbnnsum4prm  47833  bgoldbnnsum3prm  47835  bgoldbtbndlem2  47837  bgoldbtbndlem3  47838  bgoldbtbndlem4  47839  bgoldbtbnd  47840  isubgredg  47897  grimuhgr  47918  clnbgrgrim  47965  grtriprop  47972  cycl3grtrilem  47977  cycl3grtri  47978  gpgusgralem  48087  gpgedgvtx0  48092  gpgedgvtx1  48093  gpgcubic  48110  gpg5nbgr3star  48112  gpgprismgr4cycllem3  48128  upgrwlkupwlk  48171  uspgropssxp  48175  uspgrsprfo  48179  isassintop  48241  lidldomn1  48262  2zlidl  48271  2zrngamgm  48276  2zrngmmgm  48283  rngccatidALTV  48303  rngcinvALTV  48307  rhmsubcALTVlem4  48315  funcringcsetcALTV2lem9  48329  ringccatidALTV  48337  srhmsubcALTV  48356  lmodvsmdi  48410  ply1mulgsumlem1  48418  ply1mulgsumlem2  48419  lincdifsn  48456  lincsumcl  48463  lincscmcl  48464  lincext3  48488  lindslinindsimp1  48489  lindslinindsimp2lem5  48494  snlindsntor  48503  lincresunit2  48510  lincresunit3lem2  48512  zgtp1leeq  48553  elbigo2  48584  fllog2  48600  digexp  48639  dig1  48640  nn0sumshdiglemA  48651  nn0sumshdiglemB  48652  1arymaptf1  48674  2arymaptf1  48685  rrxlinec  48768  eenglngeehlnm  48771  rrx2linest  48774  itsclc0yqsol  48796  itsclc0xyqsol  48800