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  2235  nfsb4t  2503  mo4  2565  2euexv  2630  2euex  2640  raleqbidvvOLD  3314  gencl  3502  2gencl  3503  vtocl2ga  3557  vtocl2gaf  3558  vtocl3gaf  3560  vtocl3ga  3562  vtocl4g  3564  vtocl4ga  3565  rspccva  3600  2reurex  3743  2reu1  3872  rexdifi  4125  sseq0  4378  r19.2z  4470  ralf0  4489  falseral0  4491  elelpwi  4585  preqsnd  4835  prproe  4881  ssuni  4908  disji2  5103  disjiun  5107  disjxiun  5116  trintss  5248  ssexg  5293  reusv2lem3  5370  propeqop  5482  otiunsndisj  5495  rexopabb  5503  pofun  5579  solin  5588  2optocl  5750  3optocl  5751  ssrelrn  5874  elrnmpt1  5940  resieq  5977  imadifssran  6140  reuop  6282  funimaexgOLD  6623  fnun  6651  fss  6721  fun  6739  fvelimab  6950  fvmptss  6997  fvn0ssdmfun  7063  fvcofneq  7082  fmptco  7118  funsndifnop  7140  fnressn  7147  fressnfv  7149  fvn0fvelrnOLD  7152  fmptsng  7159  fvtp2g  7190  fvtp3g  7191  tpres  7192  fnex  7208  funfvima3  7227  fvf1pr  7299  isores3  7327  tfisg  7847  dmfex  7899  opreuopreu  8031  releldmdifi  8042  funeldmdif  8045  el2mpocsbcl  8082  f1o2ndf1  8119  frxp  8123  fnse  8130  frxp2  8141  frxp3  8148  poseq  8155  ressuppssdif  8182  funsssuppss  8187  mpoxopxnop0  8212  reldmtpos  8231  frrlem8  8290  fpr2a  8299  wfrfunOLD  8331  wfrlem12OLD  8332  smores  8364  tfrlem7  8395  tz7.48-2  8454  tz7.49  8457  oacl  8545  omcl  8546  oecl  8547  oarec  8572  oewordri  8602  oeworde  8603  oelim2  8605  oeoa  8607  oeoelem  8608  oeoe  8609  nnacl  8621  nnmcl  8622  nnecl  8623  nnmsucr  8635  naddoa  8712  brinxper  8746  2ecoptocl  8820  fsetprcnex  8874  undifixp  8946  ssctOLD  9064  xpf1o  9151  limensuc  9166  unfi  9183  en1eqsn  9278  ac6sfi  9290  frfi  9291  difinf  9319  imafiOLD  9324  f1dmvrnfibi  9351  f1vrnfibi  9352  suppeqfsuppbi  9389  elfiun  9440  dffi3  9441  infsupprpr  9516  xpwdomg  9597  infdiffi  9670  ttrclselem2  9738  epfrs  9743  frmin  9761  frr2  9772  rankxpsuc  9894  updjud  9946  tskwe  9962  infxpenlem  10025  fseqenlem1  10036  kmlem2  10164  nnadju  10210  cff1  10270  cflim2  10275  sornom  10289  infpssrlem4  10318  fin23lem26  10337  fin23lem30  10354  fin23lem34  10358  isf32lem11  10375  fin67  10407  isfin7-2  10408  fin1a2lem10  10421  axcc2lem  10448  axdc2lem  10460  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  iunfo  10551  tsk0  10775  gruina  10830  grur1a  10831  mulcanenq  10972  reclem2pr  11060  supsrlem  11123  supsr  11124  ax1rid  11173  negf1o  11665  mulgt1OLD  12098  lbreu  12190  nnindd  12258  nnaddcl  12261  nnmulcl  12262  nn0n0n1ge2b  12568  nn0indd  12688  fzind  12689  fnn0ind  12690  uzaddcl  12918  uzinfi  12942  nn01to3  12955  elpq  12989  xmulasslem2  13296  supxrunb1  13333  supxrunb2  13334  infmremnf  13358  infmrp1  13359  uzsubsubfz  13561  fzdif1  13620  elfz0ubfz0  13647  fz0fzdiffz0  13652  elfzmlbp  13654  fzofzim  13724  elfzom1elp1fzo  13746  ssfzo12bi  13775  fzoopth  13776  fzonfzoufzol  13784  elfznelfzob  13787  injresinjlem  13801  injresinj  13802  modaddmodup  13950  modfzo0difsn  13959  modsumfzodifsn  13960  addmodlteq  13962  om2uzlti  13966  fsequb  13991  ssnn0fi  14001  ser1const  14074  expcllem  14088  expeq0  14108  expmordi  14183  expnngt1  14257  faclbnd  14306  hashf1rn  14368  hashgadd  14393  hashunx  14402  hashnn0n0nn  14407  hashgt0elex  14417  hashss  14425  hashfzp1  14447  hashxp  14450  hashmap  14451  hashimarni  14457  seqcoll  14480  hash2exprb  14487  hashge2el2difr  14497  elss2prb  14504  hashdifsnp1  14522  fi1uzind  14523  brfi1indALT  14526  lswlgt0cl  14585  swrdnd  14670  swrdnnn0nd  14672  swrdnd0  14673  swrd0  14674  swrdsbslen  14680  swrdspsleq  14681  pfxsuff1eqwrdeq  14715  swrdswrdlem  14720  swrdswrd  14721  wrd2ind  14739  pfxccatin12lem2a  14743  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12lem3  14748  pfxccatin12  14749  pfxccat3  14750  swrdccat  14751  pfxccat3a  14754  swrdccat3blem  14755  repswswrd  14800  repswrevw  14803  cshwmodn  14811  cshwsublen  14812  cshwidxmod  14819  cshwidxmodr  14820  cshf1  14826  2cshw  14829  cshweqrep  14837  cshw1  14838  2cshwcshw  14842  cshwcshid  14844  cshwcsh2id  14845  wrdlen2i  14959  2swrd2eqwrdeq  14970  wwlktovfo  14975  relexpsucnnl  15047  rtrclreclem3  15077  rtrclreclem4  15078  relexpindlem  15080  r19.29uz  15367  caubnd  15375  sqreu  15377  climshft  15590  climub  15676  climserle  15677  sumss  15738  sumss2  15740  modfsummods  15807  o1fsum  15827  binom  15844  climcndslem1  15863  climcndslem2  15864  cvgrat  15897  clim2prod  15902  prodfn0  15908  prodfrec  15909  ntrivcvgfvn0  15913  fprodn0  15993  fprodmodd  16011  fprodefsum  16109  demoivreALT  16217  ruclem8  16253  dvdsaddre2b  16324  dvdsdivcl  16333  dvdsfac  16343  oddnn02np1  16365  oddge22np1  16366  evennn02n  16367  evennn2n  16368  m1exp1  16393  nn0o  16400  pwp1fsum  16408  flodddiv4  16432  smu01lem  16502  dvdslegcd  16521  gcdneg  16539  dfgcd2  16563  seq1st  16588  alginv  16592  lcmf  16650  lcmftp  16653  lcmfunsnlem2lem2  16656  lcmfunsnlem  16658  lcmfun  16662  ncoprmgcdne1b  16667  coprmproddvdslem  16679  coprmproddvds  16680  cncongr1  16684  prmdvdsexp  16732  prmndvdsfaclt  16742  ncoprmlnprm  16745  fvprmselgcd1  17063  prmgaplem6  17074  prmgaplem7  17075  prmgaplem8  17076  cshwshashlem1  17113  setsstruct2  17191  setsstruct  17193  inveq  17785  catsubcat  17850  initoeu2lem0  18024  initoeu2lem1  18025  funcestrcsetclem8  18157  funcestrcsetclem9  18158  fthestrcsetc  18160  fullestrcsetc  18161  funcsetcestrclem9  18173  fthsetcestrc  18175  fullsetcestrc  18176  lubss  18521  lubel  18522  mgmpropd  18627  issstrmgm  18629  mgmb1mgm1  18631  sgrpidmnd  18715  frmdgsum  18838  smndex1mndlem  18885  mgm2nsgrplem3  18896  dfgrp2  18943  cyccom  19184  gaass  19278  gsumwrev  19347  symgextf1lem  19399  symgextf1  19400  fvcosymgeq  19408  gsmsymgreq  19411  symgfixelsi  19414  pmtrprfv3  19433  symggen  19449  pmtrprfval  19466  gsumzres  19888  gsumpr  19934  gsumzunsnd  19935  srgmulgass  20175  srgbinom  20189  0ringnnzr  20483  rnghmsscmap  20588  rnghmsubcsetclem2  20590  rngcinv  20595  funcrngcsetc  20598  funcrngcsetcALT  20599  rhmsscmap  20617  rhmsubcsetclem2  20619  rhmsubcrngclem2  20625  funcringcsetc  20632  srhmsubc  20638  rhmsubclem4  20646  lmodvsmmulgdi  20852  lmodfopnelem1  20853  rmodislmodlem  20884  rngqiprngimfo  21260  cnfldmulg  21364  cnfldexp  21365  psgndiflemB  21558  assamulgscm  21859  gsumply1subr  22167  gsummoncoe1  22244  pf1ind  22291  matmulcell  22381  mat1dimscm  22411  dmatmul  22433  dmatscmcl  22439  scmataddcl  22452  scmatsubcl  22453  scmatsgrp1  22458  mavmulsolcl  22487  ma1repveval  22507  1marepvmarrepid  22511  symgmatr01lem  22589  slesolvec  22615  cramerimplem2  22620  decpmatmullem  22707  pm2mpf1  22735  mp2pm2mplem4  22745  monmat2matmon  22760  chpscmat  22778  chpscmatgsumbin  22780  fvmptnn04ifb  22787  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulgsum  22800  cpmadugsumlemF  22812  toprntopon  22861  clsss  22990  ntrss  22991  restntr  23118  cmpsublem  23335  cmpsub  23336  2ndcrest  23390  txindislem  23569  t0kq  23754  filufint  23856  fbflim2  23913  flftg  23932  alexsubALTlem4  23986  cnextfvval  24001  ustuqtop4  24181  xmettri2  24277  mettri  24289  metss  24445  tngngp3  24593  clmvscom  25039  lmmbr  25208  caublcls  25259  lmcau  25263  ovolunlem1a  25447  nulmbl2  25487  voliunlem1  25501  iunmbl  25504  volsup  25507  dvlip  25948  dvfsumle  25976  dvfsumleOLD  25977  degltlem1  26027  ply1divex  26092  plyco  26196  dgrnznn  26202  dvnply2  26245  plydivex  26255  aannenlem2  26287  aaliou3lem2  26301  ulmcau  26354  zabsle1  27257  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  gausslemma2dlem3  27329  gausslemma2dlem4  27330  2lgslem1a1  27350  2sqnn0  27399  2sqreulem1  27407  2sqreunnlem1  27410  dchrisumlem1  27450  dchrisumlem2  27451  dchrisumlem3  27452  qabvle  27586  ostthlem2  27589  ostth2lem2  27595  nosupbnd1lem5  27674  noinfbnd1lem5  27689  nocvxminlem  27739  nocvxmin  27740  slerec  27781  madebdaylemold  27853  mulsuniflem  28092  precsexlem6  28153  precsexlem7  28154  precsexlem8  28155  precsexlem9  28156  abssge0  28186  noseqind  28215  om2noseqlt  28222  om2noseqrdg  28227  n0addscl  28264  n0mulscl  28265  expscl  28330  tgjustr  28399  axeuclidlem  28887  incistruhgr  29004  umgredgprv  29032  umgrpredgv  29065  usgredgprvALT  29120  uhgr2edg  29133  usgredg2vlem2  29151  lfuhgr1v0e  29179  subgrfun  29206  umgrres1lem  29235  upgrres1  29238  fusgrfis  29255  uhgrnbgr0nb  29279  nbgr1vtx  29283  nb3grprlem1  29305  uvtx01vtx  29322  fusgrn0degnn0  29425  vtxdginducedm1lem4  29468  finsumvtxdg2size  29476  wlkl1loop  29564  wlkres  29596  lfgrwlknloop  29615  pthdadjvtx  29656  dfpth2  29657  upgr2pthnlp  29660  upgrwlkdvdelem  29664  upgrwlkdvde  29665  uhgrwkspthlem2  29682  usgr2trlspth  29689  usgr2pth  29692  pthdlem2lem  29695  cyclnumvtx  29728  lfgrn1cycl  29733  uspgrn2crct  29736  crctcshwlkn0lem3  29740  crctcshwlkn0lem4  29741  crctcshwlkn0lem5  29742  iswspthsnon  29784  wlkiswwlks1  29795  wlklnwwlkln1  29796  wlkiswwlks2  29803  wlkiswwlksupgr2  29805  wlklnwwlkln2lem  29810  wlknwwlksnbij  29816  wwlksnred  29820  wwlksnext  29821  wwlksnredwwlkn  29823  wwlksnredwwlkn0  29824  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextsurj  29828  wspthsnonn0vne  29845  wspn0  29852  wwlks2onv  29881  elwwlks2  29894  elwspths2spth  29895  rusgrnumwwlk  29903  clwwlkccatlem  29916  clwlkclwwlklem2a1  29919  clwlkclwwlklem2fv2  29923  clwlkclwwlklem2a4  29924  clwlkclwwlklem2a  29925  clwlkclwwlklem2  29927  clwlkclwwlkf1lem3  29933  clwwisshclwwslem  29941  clwwisshclwwsn  29943  erclwwlktr  29949  isclwwlknx  29963  clwwlkinwwlk  29967  clwwlkel  29973  clwwlkf  29974  clwwlkf1  29976  clwwlkfo  29977  clwwlkext2edg  29983  wwlksext2clwwlk  29984  wwlksubclwwlk  29985  clwwlknscsh  29989  erclwwlkntr  29998  eleclclwwlkn  30003  hashecclwwlkn1  30004  umgrhashecclwwlk  30005  clwwlknon0  30020  clwwlknonel  30022  clwwlknon1  30024  clwwlknonwwlknonb  30033  clwwlknonex2lem2  30035  clwwlknun  30039  clwwlkvbij  30040  upgr3v3e3cycl  30107  uhgr3cyclex  30109  upgr4cycl4dv4e  30112  eulerpath  30168  eucrctshift  30170  eucrct2eupth  30172  1to2vfriswmgr  30206  1to3vfriswmgr  30207  3cyclfrgrrn1  30212  4cycl2vnunb  30217  frgrwopreglem2  30240  frgrwopreglem3  30241  frgrwopreglem5ALT  30249  fusgr2wsp2nb  30261  2clwwlk2clwwlklem  30273  2clwwlk2clwwlk  30277  numclwwlk1lem2f1  30284  numclwwlk1lem2fo  30285  numclwwlk1  30288  clwwlknonclwlknonf1o  30289  dlwwlknondlwlknonf1o  30292  numclwlk1  30298  numclwlk2lem2f  30304  numclwlk2lem2f1o  30306  numclwwlk5  30315  frgrreg  30321  frgrregord013  30322  friendship  30326  nsnlplig  30408  nsnlpligALT  30409  isgrpo  30424  vcdi  30492  vcdir  30493  vcass  30494  nmosetre  30691  hlim2  31119  shscli  31244  chintcli  31258  dfch2  31334  spansncvi  31579  nmopsetretALT  31790  nmfnsetre  31804  lnopl  31841  lnfnl  31858  pjss2coi  32091  pjorthcoi  32096  pjscji  32097  pjssdif2i  32101  pjclem4a  32125  pj3lem1  32133  strlem5  32182  hstrlem5  32190  cvmdi  32251  mdslmd3i  32259  atcv1  32307  atcvat4i  32324  cdj3lem2a  32363  cdj3lem3a  32366  opreu2reuALT  32404  iuninc  32487  disji2f  32504  disjif2  32508  fmptcof2  32581  xrsmulgzz  32947  ofldchr  33282  1arithufdlem3  33507  esumfzf  34046  issgon  34100  voliune  34206  volfiniune  34207  rrvsum  34432  bnj228  34712  bnj1294  34794  bnj229  34861  bnj607  34893  bnj908  34908  bnj953  34916  bnj1118  34961  bnj1174  34980  bnj1388  35010  funen1cnv  35065  acycgrsubgr  35126  cvmliftlem15  35266  satfsschain  35332  satfdm  35337  satf0op  35345  fmla0xp  35351  gonarlem  35362  goalrlem  35364  satffunlem1lem1  35370  satffunlem2lem1  35372  dmopab3rexdif  35373  satefvfmla0  35386  prv1n  35399  iprodefisumlem  35703  faclimlem1  35706  dfon2lem6  35752  idinside  36048  onsucconni  36401  axc11n11r  36647  bj-brrelex12ALT  37031  bj-snmoore  37077  bj-finsumval0  37249  exlimim  37306  exellim  37308  icoreclin  37321  difunieq  37338  fvineqsneq  37376  pibt2  37381  wl-spae  37485  wl-aleq  37499  fin2so  37577  matunitlindf  37588  poimirlem4  37594  poimirlem26  37616  itg2addnclem  37641  upixp  37699  welb  37706  sdclem2  37712  metf1o  37725  sstotbnd3  37746  isbndx  37752  ismtycnv  37772  heiborlem4  37784  bfplem1  37792  opidonOLD  37822  grpomndo  37845  ax12eq  38905  ax12el  38906  cvrat4  39408  nn0addcom  42440  nn0mulcom  42444  mzpexpmpt  42715  diophren  42783  rmxypos  42918  jm2.17a  42931  jm2.17b  42932  rmygeid  42935  jm2.18  42959  jm2.25  42970  jm2.15nn0  42974  jm2.16nn0  42975  pwslnm  43065  isnumbasgrplem1  43072  dgraalem  43116  onuniintrab  43197  onsupuni  43200  onsupcl3  43204  naddonnn  43366  naddwordnexlem2  43369  relexpiidm  43675  relexpmulnn  43680  relexpmulg  43681  relexp01min  43684  relexp0a  43687  relexpxpmin  43688  clsk1indlem3  44014  grucollcld  44232  dvgrat  44284  radcnvrat  44286  sspwimpcf  44892  sspwimpcfVD  44893  e2ebindALT  44901  trfr  44935  et-sqrtnegnre  46850  fsetprcnexALT  47039  eu2ndop1stv  47102  afvfv0bi  47129  afveu  47130  afvres  47149  aovmpt4g  47178  ndmaovass  47183  ndmaovdistr  47184  afv2orxorb  47205  afv2eu  47215  imarnf1pr  47259  nltle2tri  47290  fzopredsuc  47300  subsubelfzo0  47303  2ffzoeq  47304  2tceilhalfelfzo1  47309  smonoord  47333  elsetpreimafvssdm  47348  iccpartres  47380  iccpartiltu  47384  iccpartigtl  47385  iccpartgt  47389  icceuelpartlem  47397  fargshiftf1  47403  ichnreuop  47434  ichreuopeq  47435  elsprel  47437  sprsymrelfo  47459  prproropf1olem4  47468  paireqne  47473  sbcpr  47483  reupr  47484  goldbachth  47509  fmtnoprmfac1  47527  fmtnoprmfac2  47529  prmdvdsfmtnof1lem2  47547  lighneallem2  47568  lighneallem4  47572  requad2  47585  even3prm2  47681  fpprwpprb  47702  gbegt5  47723  sbgoldbwt  47739  sbgoldbm  47746  nnsum3primesgbe  47754  wtgoldbnnsum4prm  47764  bgoldbnnsum3prm  47766  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  isubgredg  47827  grimuhgr  47848  clnbgrgrim  47895  grtriprop  47901  cycl3grtrilem  47906  cycl3grtri  47907  gpgusgralem  48008  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgcubic  48029  gpg5nbgr3star  48031  gpgprismgr4cycllem3  48044  upgrwlkupwlk  48063  uspgropssxp  48067  uspgrsprfo  48071  isassintop  48133  lidldomn1  48154  2zlidl  48163  2zrngamgm  48168  2zrngmmgm  48175  rngccatidALTV  48195  rngcinvALTV  48199  rhmsubcALTVlem4  48207  funcringcsetcALTV2lem9  48221  ringccatidALTV  48229  srhmsubcALTV  48248  lmodvsmdi  48302  ply1mulgsumlem1  48310  ply1mulgsumlem2  48311  lincdifsn  48348  lincsumcl  48355  lincscmcl  48356  lincext3  48380  lindslinindsimp1  48381  lindslinindsimp2lem5  48386  snlindsntor  48395  lincresunit2  48402  lincresunit3lem2  48404  zgtp1leeq  48445  m1modmmod  48449  elbigo2  48480  fllog2  48496  digexp  48535  dig1  48536  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  1arymaptf1  48570  2arymaptf1  48581  rrxlinec  48664  eenglngeehlnm  48667  rrx2linest  48670  itsclc0yqsol  48692  itsclc0xyqsol  48696