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  2498  mo4  2560  2euexv  2625  2euex  2635  raleqbidvvOLD  3310  gencl  3492  2gencl  3493  vtocl2ga  3547  vtocl2gaf  3548  vtocl3gaf  3550  vtocl3ga  3552  vtocl4g  3554  vtocl4ga  3555  rspccva  3590  2reurex  3734  2reu1  3863  rexdifi  4116  sseq0  4369  r19.2z  4461  ralf0  4480  falseral0  4482  elelpwi  4576  preqsnd  4826  prproe  4872  ssuni  4899  disji2  5094  disjiun  5098  disjxiun  5107  trintss  5236  ssexg  5281  reusv2lem3  5358  propeqop  5470  otiunsndisj  5483  rexopabb  5491  pofun  5567  solin  5576  2optocl  5737  3optocl  5738  ssrelrn  5861  elrnmpt1  5927  resieq  5964  imadifssran  6127  reuop  6269  funimaexgOLD  6607  fnun  6635  fss  6707  fun  6725  fvelimab  6936  fvmptss  6983  fvn0ssdmfun  7049  fvcofneq  7068  fmptco  7104  funsndifnop  7126  fnressn  7133  fressnfv  7135  fvn0fvelrnOLD  7138  fmptsng  7145  fvtp2g  7176  fvtp3g  7177  tpres  7178  fnex  7194  funfvima3  7213  fvf1pr  7285  isores3  7313  tfisg  7833  dmfex  7884  opreuopreu  8016  releldmdifi  8027  funeldmdif  8030  el2mpocsbcl  8067  f1o2ndf1  8104  frxp  8108  fnse  8115  frxp2  8126  frxp3  8133  poseq  8140  ressuppssdif  8167  funsssuppss  8172  mpoxopxnop0  8197  reldmtpos  8216  frrlem8  8275  fpr2a  8284  smores  8324  tfrlem7  8354  tz7.48-2  8413  tz7.49  8416  oacl  8502  omcl  8503  oecl  8504  oarec  8529  oewordri  8559  oeworde  8560  oelim2  8562  oeoa  8564  oeoelem  8565  oeoe  8566  nnacl  8578  nnmcl  8579  nnecl  8580  nnmsucr  8592  naddoa  8669  brinxper  8703  2ecoptocl  8784  fsetprcnex  8838  undifixp  8910  ssctOLD  9026  xpf1o  9109  limensuc  9124  unfi  9141  en1eqsn  9226  ac6sfi  9238  frfi  9239  difinf  9267  imafiOLD  9272  f1dmvrnfibi  9299  f1vrnfibi  9300  suppeqfsuppbi  9337  elfiun  9388  dffi3  9389  infsupprpr  9464  xpwdomg  9545  infdiffi  9618  ttrclselem2  9686  epfrs  9691  frmin  9709  frr2  9720  rankxpsuc  9842  updjud  9894  tskwe  9910  infxpenlem  9973  fseqenlem1  9984  kmlem2  10112  nnadju  10158  cff1  10218  cflim2  10223  sornom  10237  infpssrlem4  10266  fin23lem26  10285  fin23lem30  10302  fin23lem34  10306  isf32lem11  10323  fin67  10355  isfin7-2  10356  fin1a2lem10  10369  axcc2lem  10396  axdc2lem  10408  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  iunfo  10499  tsk0  10723  gruina  10778  grur1a  10779  mulcanenq  10920  reclem2pr  11008  supsrlem  11071  supsr  11072  ax1rid  11121  negf1o  11615  mulgt1OLD  12048  lbreu  12140  nnindd  12213  nnaddcl  12216  nnmulcl  12217  nn0n0n1ge2b  12518  nn0indd  12638  fzind  12639  fnn0ind  12640  uzaddcl  12870  uzinfi  12894  nn01to3  12907  elpq  12941  xmulasslem2  13249  supxrunb1  13286  supxrunb2  13287  infmremnf  13311  infmrp1  13312  uzsubsubfz  13514  fzdif1  13573  elfz0ubfz0  13600  fz0fzdiffz0  13605  elfzmlbp  13607  fzofzim  13677  elfzom1elp1fzo  13700  ssfzo12bi  13729  fzoopth  13730  fzonfzoufzol  13738  elfznelfzob  13741  injresinjlem  13755  injresinj  13756  modaddmodup  13906  modfzo0difsn  13915  modsumfzodifsn  13916  addmodlteq  13918  om2uzlti  13922  fsequb  13947  ssnn0fi  13957  ser1const  14030  expcllem  14044  expeq0  14064  expmordi  14139  expnngt1  14213  faclbnd  14262  hashf1rn  14324  hashgadd  14349  hashunx  14358  hashnn0n0nn  14363  hashgt0elex  14373  hashss  14381  hashfzp1  14403  hashxp  14406  hashmap  14407  hashimarni  14413  seqcoll  14436  hash2exprb  14443  hashge2el2difr  14453  elss2prb  14460  hashdifsnp1  14478  fi1uzind  14479  brfi1indALT  14482  lswlgt0cl  14541  swrdnd  14626  swrdnnn0nd  14628  swrdnd0  14629  swrd0  14630  swrdsbslen  14636  swrdspsleq  14637  pfxsuff1eqwrdeq  14671  swrdswrdlem  14676  swrdswrd  14677  wrd2ind  14695  pfxccatin12lem2a  14699  swrdccatin2  14701  pfxccatin12lem2  14703  pfxccatin12lem3  14704  pfxccatin12  14705  pfxccat3  14706  swrdccat  14707  pfxccat3a  14710  swrdccat3blem  14711  repswswrd  14756  repswrevw  14759  cshwmodn  14767  cshwsublen  14768  cshwidxmod  14775  cshwidxmodr  14776  cshf1  14782  2cshw  14785  cshweqrep  14793  cshw1  14794  2cshwcshw  14798  cshwcshid  14800  cshwcsh2id  14801  wrdlen2i  14915  2swrd2eqwrdeq  14926  wwlktovfo  14931  relexpsucnnl  15003  rtrclreclem3  15033  rtrclreclem4  15034  relexpindlem  15036  r19.29uz  15324  caubnd  15332  sqreu  15334  climshft  15549  climub  15635  climserle  15636  sumss  15697  sumss2  15699  modfsummods  15766  o1fsum  15786  binom  15803  climcndslem1  15822  climcndslem2  15823  cvgrat  15856  clim2prod  15861  prodfn0  15867  prodfrec  15868  ntrivcvgfvn0  15872  fprodn0  15952  fprodmodd  15970  fprodefsum  16068  demoivreALT  16176  ruclem8  16212  dvdsaddre2b  16284  dvdsdivcl  16293  dvdsfac  16303  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  m1exp1  16353  nn0o  16360  pwp1fsum  16368  flodddiv4  16392  smu01lem  16462  dvdslegcd  16481  gcdneg  16499  dfgcd2  16523  seq1st  16548  alginv  16552  lcmf  16610  lcmftp  16613  lcmfunsnlem2lem2  16616  lcmfunsnlem  16618  lcmfun  16622  ncoprmgcdne1b  16627  coprmproddvdslem  16639  coprmproddvds  16640  cncongr1  16644  prmdvdsexp  16692  prmndvdsfaclt  16702  ncoprmlnprm  16705  fvprmselgcd1  17023  prmgaplem6  17034  prmgaplem7  17035  prmgaplem8  17036  cshwshashlem1  17073  setsstruct2  17151  setsstruct  17153  inveq  17743  catsubcat  17808  initoeu2lem0  17982  initoeu2lem1  17983  funcestrcsetclem8  18115  funcestrcsetclem9  18116  fthestrcsetc  18118  fullestrcsetc  18119  funcsetcestrclem9  18131  fthsetcestrc  18133  fullsetcestrc  18134  lubss  18479  lubel  18480  mgmpropd  18585  issstrmgm  18587  mgmb1mgm1  18589  sgrpidmnd  18673  frmdgsum  18796  smndex1mndlem  18843  mgm2nsgrplem3  18854  dfgrp2  18901  cyccom  19142  gaass  19236  gsumwrev  19305  symgextf1lem  19357  symgextf1  19358  fvcosymgeq  19366  gsmsymgreq  19369  symgfixelsi  19372  pmtrprfv3  19391  symggen  19407  pmtrprfval  19424  gsumzres  19846  gsumpr  19892  gsumzunsnd  19893  srgmulgass  20133  srgbinom  20147  0ringnnzr  20441  rnghmsscmap  20546  rnghmsubcsetclem2  20548  rngcinv  20553  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap  20575  rhmsubcsetclem2  20577  rhmsubcrngclem2  20583  funcringcsetc  20590  srhmsubc  20596  rhmsubclem4  20604  lmodvsmmulgdi  20810  lmodfopnelem1  20811  rmodislmodlem  20842  rngqiprngimfo  21218  cnfldmulg  21322  cnfldexp  21323  psgndiflemB  21516  assamulgscm  21817  gsumply1subr  22125  gsummoncoe1  22202  pf1ind  22249  matmulcell  22339  mat1dimscm  22369  dmatmul  22391  dmatscmcl  22397  scmataddcl  22410  scmatsubcl  22411  scmatsgrp1  22416  mavmulsolcl  22445  ma1repveval  22465  1marepvmarrepid  22469  symgmatr01lem  22547  slesolvec  22573  cramerimplem2  22578  decpmatmullem  22665  pm2mpf1  22693  mp2pm2mplem4  22703  monmat2matmon  22718  chpscmat  22736  chpscmatgsumbin  22738  fvmptnn04ifb  22745  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulgsum  22758  cpmadugsumlemF  22770  toprntopon  22819  clsss  22948  ntrss  22949  restntr  23076  cmpsublem  23293  cmpsub  23294  2ndcrest  23348  txindislem  23527  t0kq  23712  filufint  23814  fbflim2  23871  flftg  23890  alexsubALTlem4  23944  cnextfvval  23959  ustuqtop4  24139  xmettri2  24235  mettri  24247  metss  24403  tngngp3  24551  clmvscom  24997  lmmbr  25165  caublcls  25216  lmcau  25220  ovolunlem1a  25404  nulmbl2  25444  voliunlem1  25458  iunmbl  25461  volsup  25464  dvlip  25905  dvfsumle  25933  dvfsumleOLD  25934  degltlem1  25984  ply1divex  26049  plyco  26153  dgrnznn  26159  dvnply2  26202  plydivex  26212  aannenlem2  26244  aaliou3lem2  26258  ulmcau  26311  zabsle1  27214  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem3  27286  gausslemma2dlem4  27287  2lgslem1a1  27307  2sqnn0  27356  2sqreulem1  27364  2sqreunnlem1  27367  dchrisumlem1  27407  dchrisumlem2  27408  dchrisumlem3  27409  qabvle  27543  ostthlem2  27546  ostth2lem2  27552  nosupbnd1lem5  27631  noinfbnd1lem5  27646  nocvxminlem  27696  nocvxmin  27697  slerec  27738  madebdaylemold  27816  mulsuniflem  28059  precsexlem6  28121  precsexlem7  28122  precsexlem8  28123  precsexlem9  28124  abssge0  28154  noseqind  28193  om2noseqlt  28200  om2noseqrdg  28205  n0addscl  28243  n0mulscl  28244  onsfi  28254  expscllem  28323  tgjustr  28408  axeuclidlem  28896  incistruhgr  29013  umgredgprv  29041  umgrpredgv  29074  usgredgprvALT  29129  uhgr2edg  29142  usgredg2vlem2  29160  lfuhgr1v0e  29188  subgrfun  29215  umgrres1lem  29244  upgrres1  29247  fusgrfis  29264  uhgrnbgr0nb  29288  nbgr1vtx  29292  nb3grprlem1  29314  uvtx01vtx  29331  fusgrn0degnn0  29434  vtxdginducedm1lem4  29477  finsumvtxdg2size  29485  wlkl1loop  29573  wlkres  29605  lfgrwlknloop  29624  pthdadjvtx  29665  dfpth2  29666  upgr2pthnlp  29669  upgrwlkdvdelem  29673  upgrwlkdvde  29674  uhgrwkspthlem2  29691  usgr2trlspth  29698  usgr2pth  29701  pthdlem2lem  29704  cyclnumvtx  29737  lfgrn1cycl  29742  uspgrn2crct  29745  crctcshwlkn0lem3  29749  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  iswspthsnon  29793  wlkiswwlks1  29804  wlklnwwlkln1  29805  wlkiswwlks2  29812  wlkiswwlksupgr2  29814  wlklnwwlkln2lem  29819  wlknwwlksnbij  29825  wwlksnred  29829  wwlksnext  29830  wwlksnredwwlkn  29832  wwlksnredwwlkn0  29833  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextsurj  29837  wspthsnonn0vne  29854  wspn0  29861  wwlks2onv  29890  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlk  29912  clwwlkccatlem  29925  clwlkclwwlklem2a1  29928  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2a4  29933  clwlkclwwlklem2a  29934  clwlkclwwlklem2  29936  clwlkclwwlkf1lem3  29942  clwwisshclwwslem  29950  clwwisshclwwsn  29952  erclwwlktr  29958  isclwwlknx  29972  clwwlkinwwlk  29976  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  clwwlkfo  29986  clwwlkext2edg  29992  wwlksext2clwwlk  29993  wwlksubclwwlk  29994  clwwlknscsh  29998  erclwwlkntr  30007  eleclclwwlkn  30012  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwwlknon0  30029  clwwlknonel  30031  clwwlknon1  30033  clwwlknonwwlknonb  30042  clwwlknonex2lem2  30044  clwwlknun  30048  clwwlkvbij  30049  upgr3v3e3cycl  30116  uhgr3cyclex  30118  upgr4cycl4dv4e  30121  eulerpath  30177  eucrctshift  30179  eucrct2eupth  30181  1to2vfriswmgr  30215  1to3vfriswmgr  30216  3cyclfrgrrn1  30221  4cycl2vnunb  30226  frgrwopreglem2  30249  frgrwopreglem3  30250  frgrwopreglem5ALT  30258  fusgr2wsp2nb  30270  2clwwlk2clwwlklem  30282  2clwwlk2clwwlk  30286  numclwwlk1lem2f1  30293  numclwwlk1lem2fo  30294  numclwwlk1  30297  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  numclwlk1  30307  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  numclwwlk5  30324  frgrreg  30330  frgrregord013  30331  friendship  30335  nsnlplig  30417  nsnlpligALT  30418  isgrpo  30433  vcdi  30501  vcdir  30502  vcass  30503  nmosetre  30700  hlim2  31128  shscli  31253  chintcli  31267  dfch2  31343  spansncvi  31588  nmopsetretALT  31799  nmfnsetre  31813  lnopl  31850  lnfnl  31867  pjss2coi  32100  pjorthcoi  32105  pjscji  32106  pjssdif2i  32110  pjclem4a  32134  pj3lem1  32142  strlem5  32191  hstrlem5  32199  cvmdi  32260  mdslmd3i  32268  atcv1  32316  atcvat4i  32333  cdj3lem2a  32372  cdj3lem3a  32375  opreu2reuALT  32413  iuninc  32496  disji2f  32513  disjif2  32517  fmptcof2  32588  xrsmulgzz  32954  ofldchr  33299  1arithufdlem3  33524  esumfzf  34066  issgon  34120  voliune  34226  volfiniune  34227  rrvsum  34452  bnj228  34732  bnj1294  34814  bnj229  34881  bnj607  34913  bnj908  34928  bnj953  34936  bnj1118  34981  bnj1174  35000  bnj1388  35030  funen1cnv  35085  acycgrsubgr  35152  cvmliftlem15  35292  satfsschain  35358  satfdm  35363  satf0op  35371  fmla0xp  35377  gonarlem  35388  goalrlem  35390  satffunlem1lem1  35396  satffunlem2lem1  35398  dmopab3rexdif  35399  satefvfmla0  35412  prv1n  35425  iprodefisumlem  35734  faclimlem1  35737  dfon2lem6  35783  idinside  36079  onsucconni  36432  axc11n11r  36678  bj-brrelex12ALT  37062  bj-snmoore  37108  bj-finsumval0  37280  exlimim  37337  exellim  37339  icoreclin  37352  difunieq  37369  fvineqsneq  37407  pibt2  37412  wl-spae  37516  wl-aleq  37530  fin2so  37608  matunitlindf  37619  poimirlem4  37625  poimirlem26  37647  itg2addnclem  37672  upixp  37730  welb  37737  sdclem2  37743  metf1o  37756  sstotbnd3  37777  isbndx  37783  ismtycnv  37803  heiborlem4  37815  bfplem1  37823  opidonOLD  37853  grpomndo  37876  ax12eq  38941  ax12el  38942  cvrat4  39444  nn0addcom  42457  nn0mulcom  42461  mzpexpmpt  42740  diophren  42808  rmxypos  42943  jm2.17a  42956  jm2.17b  42957  rmygeid  42960  jm2.18  42984  jm2.25  42995  jm2.15nn0  42999  jm2.16nn0  43000  pwslnm  43090  isnumbasgrplem1  43097  dgraalem  43141  onuniintrab  43222  onsupuni  43225  onsupcl3  43229  naddonnn  43391  naddwordnexlem2  43394  relexpiidm  43700  relexpmulnn  43705  relexpmulg  43706  relexp01min  43709  relexp0a  43712  relexpxpmin  43713  clsk1indlem3  44039  grucollcld  44256  dvgrat  44308  radcnvrat  44310  sspwimpcf  44916  sspwimpcfVD  44917  e2ebindALT  44925  trfr  44959  et-sqrtnegnre  46878  fsetprcnexALT  47067  eu2ndop1stv  47130  afvfv0bi  47157  afveu  47158  afvres  47177  aovmpt4g  47206  ndmaovass  47211  ndmaovdistr  47212  afv2orxorb  47233  afv2eu  47243  imarnf1pr  47287  nltle2tri  47318  fzopredsuc  47328  subsubelfzo0  47331  2ffzoeq  47332  2tceilhalfelfzo1  47337  m1modmmod  47363  smonoord  47376  elsetpreimafvssdm  47391  iccpartres  47423  iccpartiltu  47427  iccpartigtl  47428  iccpartgt  47432  icceuelpartlem  47440  fargshiftf1  47446  ichnreuop  47477  ichreuopeq  47478  elsprel  47480  sprsymrelfo  47502  prproropf1olem4  47511  paireqne  47516  sbcpr  47526  reupr  47527  goldbachth  47552  fmtnoprmfac1  47570  fmtnoprmfac2  47572  prmdvdsfmtnof1lem2  47590  lighneallem2  47611  lighneallem4  47615  requad2  47628  even3prm2  47724  fpprwpprb  47745  gbegt5  47766  sbgoldbwt  47782  sbgoldbm  47789  nnsum3primesgbe  47797  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbndlem4  47813  bgoldbtbnd  47814  isubgredg  47870  grimuhgr  47891  clnbgrgrim  47938  grtriprop  47944  cycl3grtrilem  47949  cycl3grtri  47950  gpgusgralem  48051  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgcubic  48074  gpg5nbgr3star  48076  gpgprismgr4cycllem3  48091  upgrwlkupwlk  48132  uspgropssxp  48136  uspgrsprfo  48140  isassintop  48202  lidldomn1  48223  2zlidl  48232  2zrngamgm  48237  2zrngmmgm  48244  rngccatidALTV  48264  rngcinvALTV  48268  rhmsubcALTVlem4  48276  funcringcsetcALTV2lem9  48290  ringccatidALTV  48298  srhmsubcALTV  48317  lmodvsmdi  48371  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  lincdifsn  48417  lincsumcl  48424  lincscmcl  48425  lincext3  48449  lindslinindsimp1  48450  lindslinindsimp2lem5  48455  snlindsntor  48464  lincresunit2  48471  lincresunit3lem2  48473  zgtp1leeq  48514  elbigo2  48545  fllog2  48561  digexp  48600  dig1  48601  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  1arymaptf1  48635  2arymaptf1  48646  rrxlinec  48729  eenglngeehlnm  48732  rrx2linest  48735  itsclc0yqsol  48757  itsclc0xyqsol  48761