Theorem impcom 413

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 33	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 412	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpan9  516  anbiim  653  bianir  1074  19.29r  1907  19.41v  1982  19.41  2272  nfsb4t  2529  mo4  2592  2euexv  2657  2euex  2667  gencl  3492  2gencl  3493  vtocl2ga  3538  vtocl2gaf  3539  vtocl3gaf  3540  vtocl3ga  3541  vtocl4g  3542  vtocl4ga  3543  rspccva  3576  2reurex  3718  2reu1  3845  rexdifi  4097  r19.2z  4455  falseral0OLD  4471  elelpwi  4567  preqsnd  4819  prproe  4865  ssuni  4893  disji2  5087  disjiun  5091  disjxiun  5100  trintss  5231  ssexgOLD  5285  reusv2lem3  5362  propeqop  5479  otiunsndisj  5493  rexopabb  5502  pofun  5577  solin  5586  2optocl  5747  3optocl  5748  ssrelrn  5876  elrnmpt1  5942  resieq  5981  imadifssranOLDOLD  6202  reuop  6295  fnun  6651  fss  6724  fun  6742  fvelimab  6955  fvmptss  7004  fvn0ssdmfun  7072  fvcofneq  7091  fmptco  7128  funsndifnop  7153  fnressn  7160  fressnfv  7162  fmptsng  7171  fvtp2g  7202  fvtp3g  7203  tpres  7205  fnex  7221  funfvima3  7240  fvf1pr  7313  isores3  7341  tfisg  7863  dmfex  7915  opreuopreu  8044  releldmdifi  8054  funeldmdif  8057  el2mpocsbcl  8094  f1o2ndf1  8131  frxp  8136  fnse  8143  frxp2  8154  frxp3  8161  poseq  8168  ressuppssdif  8195  funsssuppss  8200  mpoxopxnop0  8225  reldmtpos  8244  frrlem8  8304  fpr2a  8313  smores  8353  tfrlem7  8384  onelfvnef1  8442  tz7.48-2  8445  tz7.49  8448  oacl  8536  omcl  8537  oecl  8538  oarec  8563  oewordri  8594  oeworde  8595  oelim2  8597  oeoa  8599  oeoelem  8600  oeoe  8601  nnacl  8613  nnmcl  8614  nnecl  8615  nnmsucr  8627  naddoa  8705  brinxper  8740  2ecoptocl  8822  fsetprcnex  8877  undifixp  8955  funen1cnv  9049  xpf1o  9151  limensuc  9166  unfi  9179  en1eqsn  9259  ac6sfi  9268  frfi  9269  difinf  9296  f1dmvrnfibi  9323  f1vrnfibi  9324  suppeqfsuppbi  9364  elfiun  9415  dffi3  9416  infsupprpr  9491  xpwdomg  9572  infdiffi  9652  ttrclselem2  9720  epfrs  9725  frmin  9746  frr2  9757  rankxpsuc  9892  rankfilimbi  9895  r1filimi  9896  updjud  10008  tskwe  10024  infxpenlem  10085  fseqenlem1  10096  kmlem2  10223  nnadju  10269  cff1  10329  cflim2  10334  sornom  10348  infpssrlem4  10377  fin23lem26  10396  fin23lem30  10413  fin23lem34  10417  isf32lem11  10434  fin67  10466  isfin7-2  10467  fin1a2lem10  10480  axcc2lem  10507  axdc2lem  10519  axdc3lem2  10522  axdc3lem4  10524  axdc4lem  10526  iunfo  10616  tsk0  10841  gruina  10896  grur1a  10897  mulcanenq  11038  reclem2pr  11126  supsrlem  11189  supsr  11190  ax1rid  11239  negf1o  11739  lbreu  12260  nnindd  12348  nnaddcl  12351  nnmulcl  12352  nn0n0n1ge2b  12668  nn0indd  12789  fzind  12790  fnn0ind  12791  uzaddcl  13024  uzinfi  13048  nn01to3  13061  elpq  13096  xmulasslem2  13405  supxrunb1  13442  supxrunb2  13443  infmremnf  13467  infmrp1  13468  uzsubsubfz  13673  fzdif1  13732  elfz0ubfz0  13759  fz0fzdiffz0  13764  elfzmlbp  13766  fzofzim  13837  elfzom1elp1fzo  13860  ssfzo12bi  13889  fzoopth  13890  fzonfzoufzol  13899  elfznelfzob  13902  injresinjlem  13918  injresinj  13919  modaddmodup  14070  modfzo0difsn  14079  modsumfzodifsn  14080  addmodlteq  14082  om2uzlti  14086  fsequb  14111  ssnn0fi  14121  ser1const  14194  expcllem  14208  expeq0  14228  expmordi  14303  expnngt1  14378  faclbnd  14427  hashf1rn  14489  hashgadd  14514  hashunx  14523  hashnn0n0nn  14528  hashgt0elex  14538  hashss  14546  hashfzp1  14569  hashxp  14572  hashmap  14573  hashimarni  14579  seqcoll  14602  hash2exprb  14609  hashge2el2difr  14619  elss2prb  14626  hashdifsnp1  14644  fi1uzind  14645  brfi1indALT  14648  lswlgt0cl  14707  swrdnd  14797  swrdnnn0nd  14799  swrdnd0  14800  swrd0  14801  swrdsbslen  14807  swrdspsleq  14808  pfxsuff1eqwrdeq  14841  swrdswrdlem  14846  swrdswrd  14847  wrd2ind  14865  pfxccatin12lem2a  14869  swrdccatin2  14871  pfxccatin12lem2  14873  pfxccatin12lem3  14874  pfxccatin12  14875  pfxccat3  14876  swrdccat  14877  pfxccat3a  14880  swrdccat3blem  14881  repswswrd  14928  repswrevw  14931  cshwmodn  14939  cshwsublen  14940  cshwidxmod  14947  cshwidxmodr  14948  cshf1  14954  2cshw  14957  cshweqrep  14965  cshw1  14966  2cshwcshw  14969  cshwcshid  14971  cshwcsh2id  14972  wrdlen2i  15086  2swrd2eqwrdeq  15099  wwlktovfo  15104  relexpsucnnl  15176  rtrclreclem3  15206  rtrclreclem4  15207  relexpindlem  15209  r19.29uz  15511  caubnd  15519  sqreu  15521  climshft  15736  climub  15822  climserle  15823  sumss  15883  sumss2  15885  modfsummods  15953  o1fsum  15973  binom  15992  climcndslem1  16011  climcndslem2  16012  cvgrat  16045  clim2prod  16050  prodfn0  16056  prodfrec  16057  ntrivcvgfvn0  16061  fprodn0  16139  fprodmodd  16157  fprodefsum  16254  demoivreALT  16362  ruclem8  16398  dvdsaddre2b  16470  dvdsdivcl  16479  dvdsfac  16489  oddnn02np1  16511  oddge22np1  16512  evennn02n  16513  evennn2n  16514  m1exp1  16539  nn0o  16546  pwp1fsum  16554  flodddiv4  16578  smu01lem  16648  dvdslegcd  16667  gcdneg  16687  dfgcd2  16712  seq1st  16739  alginv  16743  lcmf  16801  lcmftp  16804  lcmfunsnlem2lem2  16807  lcmfunsnlem  16809  lcmfun  16813  ncoprmgcdne1b  16818  coprmproddvdslem  16830  coprmproddvds  16831  cncongr1  16835  prmdvdsexp  16884  prmndvdsfaclt  16894  ncoprmlnprm  16897  fvprmselgcd1  17216  prmgaplem6  17227  prmgaplem7  17228  prmgaplem8  17229  cshwshashlem1  17266  setsstruct2  17345  setsstruct  17347  inveq  17942  catsubcat  18007  initoeu2lem0  18181  initoeu2lem1  18182  funcestrcsetclem8  18314  funcestrcsetclem9  18315  fthestrcsetc  18317  fullestrcsetc  18318  funcsetcestrclem9  18330  fthsetcestrc  18332  fullsetcestrc  18333  lubss  18680  lubel  18681  mgmpropd  18822  issstrmgm  18824  mgmb1mgm1  18826  mgmidpfod  18850  sgrpidmnd  18921  frmdgsum  19051  smndex1mndlem  19101  mgm2nsgrplem3  19112  dfgrp2  19166  cyccom  19411  gaass  19504  gsumwrev  19573  symgextf1lem  19627  symgextf1  19628  fvcosymgeq  19636  gsmsymgreq  19639  symgfixelsi  19642  pmtrprfv3  19661  symggen  19677  pmtrprfval  19694  gsumzres  20116  gsumpr  20162  gsumzunsnd  20163  srgmulgass  20436  srgbinom  20450  0ringnnzr  20769  rnghmsscmap  20875  rnghmsubcsetclem2  20877  rngcinv  20882  funcrngcsetc  20885  funcrngcsetcALT  20886  rhmsscmap  20904  rhmsubcsetclem2  20906  rhmsubcrngclem2  20912  funcringcsetc  20919  srhmsubc  20925  rhmsubclem4  20933  lmodvsmmulgdi  21165  lmodfopnelem1  21166  rmodislmodlem  21197  rngqiprngimfo  21590  cnfldmulg  21703  cnfldexp  21704  ofldchr  21875  psgndiflemB  21899  assamulgscm  22202  gsumply1subr  22544  gsummoncoe1  22619  pf1ind  22666  matmulcell  22753  mat1dimscm  22783  dmatmul  22805  dmatscmcl  22811  scmataddcl  22824  scmatsubcl  22825  scmatsgrp1  22830  mavmulsolcl  22859  ma1repveval  22879  1marepvmarrepid  22883  symgmatr01lem  22961  matunitlindf  22989  slesolvec  22990  cramerimplem2  22995  decpmatmullem  23082  pm2mpf1  23110  mp2pm2mplem4  23120  monmat2matmon  23135  chpscmat  23153  chpscmatgsumbin  23155  fvmptnn04ifb  23162  chfacfscmul0  23169  chfacfscmulgsum  23171  chfacfpmmul0  23173  chfacfpmmulgsum  23175  cpmadugsumlemF  23187  toprntopon  23236  clsss  23365  ntrss  23366  restntr  23493  cmpsublem  23710  cmpsub  23711  2ndcrest  23765  txindislem  23945  t0kq  24130  filufint  24232  fbflim2  24289  flftg  24308  alexsubALTlem4  24362  cnextfvval  24377  ustuqtop4  24556  xmettri2  24652  mettri  24664  metss  24820  tngngp3  24968  clmvscom  25404  lmmbr  25572  caublcls  25623  lmcau  25627  ovolunlem1a  25810  nulmbl2  25850  voliunlem1  25864  iunmbl  25867  volsup  25870  dvlip  26306  dvfsumle  26334  degltlem1  26383  ply1divex  26448  plyco  26553  dgrnznn  26559  dvnply2  26601  plydivex  26611  aannenlem2  26649  aaliou3lem2  26663  ulmcau  26715  zabsle1  27616  gausslemma2dlem1a  27685  gausslemma2dlem2  27687  gausslemma2dlem3  27688  gausslemma2dlem4  27689  2lgslem1a1  27709  2sqnn0  27758  2sqreulem1  27766  2sqreunnlem1  27769  dchrisumlem1  27809  dchrisumlem2  27810  dchrisumlem3  27811  qabvle  27945  ostthlem2  27948  ostth2lem2  27954  nosupbnd1lem5  28062  noinfbnd1lem5  28077  nocvxminlem  28133  lesrec  28178  madebdaylemold  28277  mulsuniflem  28528  precsexlem6  28591  precsexlem7  28592  precsexlem8  28593  precsexlem9  28594  abssge0  28624  noseqind  28671  om2noseqlt  28678  om2noseqrdg  28683  n0addscl  28723  n0mulscl  28724  onsfi  28735  oldfib  28756  expscllem  28809  pw2cut2  28841  z12zsodd  28861  tgjustr  28929  axeuclidlem  29533  incistruhgr  29650  umgredgprv  29678  umgrpredgv  29711  usgredgprvALT  29769  uhgr2edg  29782  usgredg2vlem2  29800  lfuhgr1v0e  29828  subgrfun  29855  umgrres1lem  29884  upgrres1  29887  fusgrfis  29904  uhgrnbgr0nb  29928  nbgr1vtx  29932  nb3grprlem1  29954  uvtx01vtx  29971  fusgrn0degnn0  30073  vtxdginducedm1lem4  30116  finsumvtxdg2size  30124  wlkl1loop  30211  wlkres  30242  lfgrwlknloop  30265  pthdadjvtx  30306  dfpth2  30307  upgr2pthnlp  30311  upgrwlkdvdelem  30315  upgrwlkdvde  30316  uhgrwkspthlem2  30333  usgr2trlspth  30340  usgr2pth  30343  pthdlem2lem  30346  cyclnumvtx  30381  lfgrn1cycl  30387  uspgrn2crct  30390  crctcshwlkn0lem3  30394  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  iswspthsnon  30438  wlkiswwlks1  30449  wlklnwwlkln1  30450  wlkiswwlks2  30457  wlkiswwlksupgr2  30459  wlklnwwlkln2lem  30464  wlknwwlksnbij  30470  wwlksnred  30474  wwlksnext  30475  wwlksnredwwlkn  30477  wwlksnredwwlkn0  30478  wwlksnextfun  30480  wwlksnextinj  30481  wwlksnextsurj  30482  wspthsnonn0vne  30499  wspn0  30506  wwlks2onv  30535  elwwlks2  30551  elwspths2spth  30552  rusgrnumwwlk  30560  clwwlkccatlem  30573  clwlkclwwlklem2a1  30576  clwlkclwwlklem2fv2  30580  clwlkclwwlklem2a4  30581  clwlkclwwlklem2a  30582  clwlkclwwlklem2  30584  clwlkclwwlkf1lem3  30590  clwwisshclwwslem  30598  clwwisshclwwsn  30600  erclwwlktr  30606  isclwwlknx  30620  clwwlkinwwlk  30624  clwwlkel  30630  clwwlkf  30631  clwwlkf1  30633  clwwlkfo  30634  clwwlkext2edg  30640  wwlksext2clwwlk  30641  wwlksubclwwlk  30642  clwwlknscsh  30646  erclwwlkntr  30655  eleclclwwlkn  30660  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  clwwlknon0  30677  clwwlknonel  30679  clwwlknon1  30681  clwwlknonwwlknonb  30690  clwwlknonex2lem2  30692  clwwlknun  30696  clwwlkvbij  30697  upgr3v3e3cycl  30774  uhgr3cyclex  30776  upgr4cycl4dv4e  30779  eulerpath  30835  eucrctshift  30837  eucrct2eupth  30839  1to2vfriswmgr  30873  1to3vfriswmgr  30874  3cyclfrgrrn1  30879  4cycl2vnunb  30884  frgrwopreglem2  30907  frgrwopreglem3  30908  frgrwopreglem5ALT  30916  fusgr2wsp2nb  30928  2clwwlk2clwwlklem  30940  2clwwlk2clwwlk  30944  numclwwlk1lem2f1  30951  numclwwlk1lem2fo  30952  numclwwlk1  30955  clwwlknonclwlknonf1o  30956  dlwwlknondlwlknonf1o  30959  numclwlk1  30965  numclwlk2lem2f  30971  numclwlk2lem2f1o  30973  numclwwlk5  30982  frgrreg  30988  frgrregord013  30989  friendship  30993  nsnlplig  31076  nsnlpligALT  31077  isgrpo  31092  vcdi  31160  vcdir  31161  vcass  31162  nmosetre  31359  hlim2  31787  shscli  31912  chintcli  31926  dfch2  32002  spansncvi  32247  nmopsetretALT  32458  nmfnsetre  32472  lnopl  32509  lnfnl  32526  pjss2coi  32759  pjorthcoi  32764  pjscji  32765  pjssdif2i  32769  pjclem4a  32793  pj3lem1  32801  strlem5  32850  hstrlem5  32858  cvmdi  32919  mdslmd3i  32927  atcv1  32975  atcvat4i  32992  cdj3lem2a  33031  cdj3lem3a  33034  opreu2reuALT  33066  iuninc  33148  disji2f  33164  disjif2  33168  fmptcof2  33244  xrsmulgzz  33563  1arithufdlem3  34071  esumfzf  34694  issgon  34748  voliune  34855  volfiniune  34856  rrvsum  35079  bnj228  35359  bnj1294  35440  bnj229  35507  bnj607  35539  bnj908  35554  bnj953  35562  bnj1118  35607  bnj1174  35626  bnj1388  35656  trssfir1om  35726  trssfir1omregs  35787  acycgrsubgr  35902  cvmliftlem15  36042  satfsschain  36108  satfdm  36113  satf0op  36121  fmla0xp  36127  gonarlem  36138  goalrlem  36140  satffunlem1lem1  36146  satffunlem2lem1  36148  dmopab3rexdif  36149  satefvfmla0  36162  prv1n  36175  iprodefisumlem  36484  faclimlem1  36487  dfon2lem6  36530  idinside  36829  onsucconni  37205  axuntco  37247  ttcmin  37264  elttctr  37273  dfttc2g  37274  bj-cbvew  37521  axc11n11r  37565  bj-brrelex12ALT  37962  bj-snmoore  38014  bj-finsumval0  38186  exlimim  38245  exellim  38247  icoreclin  38260  difunieq  38277  fvineqsneq  38315  pibt2  38320  wl-spae  38433  wl-aleq  38447  fin2so  38510  poimirlem4  38522  poimirlem26  38544  itg2addnclem  38569  upixp  38643  welb  38650  sdclem2  38656  metf1o  38669  sstotbnd3  38690  isbndx  38696  ismtycnv  38716  heiborlem4  38728  bfplem1  38736  opidonOLD  38766  grpomndo  38789  eldisjdmqsim2  39728  ax12eq  39978  ax12el  39979  cvrat4  40480  nn0addcom  43506  nn0mulcom  43510  mzpexpmpt  43735  diophren  43799  rmxypos  43933  jm2.17a  43946  jm2.17b  43947  rmygeid  43950  jm2.18  43974  jm2.25  43985  jm2.15nn0  43989  jm2.16nn0  43990  pwslnm  44080  isnumbasgrplem1  44087  dgraalem  44131  onuniintrab  44212  onsupuni  44215  onsupcl3  44219  naddonnn  44381  naddwordnexlem2  44384  relexpiidm  44689  relexpmulnn  44694  relexpmulg  44695  relexp01min  44698  relexp0a  44701  relexpxpmin  44702  clsk1indlem3  45028  grucollcld  45229  dvgrat  45281  radcnvrat  45283  sspwimpcf  45887  sspwimpcfVD  45888  e2ebindALT  45896  trfr  45930  et-sqrtnegnre  47852  fsetprcnexALT  48101  eu2ndop1stv  48164  afvfv0bi  48191  afveu  48192  afvres  48211  aovmpt4g  48240  ndmaovass  48245  ndmaovdistr  48246  afv2orxorb  48267  afv2eu  48277  imarnf1pr  48321  nltle2tri  48352  fzopredsuc  48363  subsubelfzo0  48366  2ffzoeq  48367  2tceilhalfelfzo1  48375  m1modmmod  48403  smonoord  48416  elsetpreimafvssdm  48437  iccpartres  48469  iccpartiltu  48473  iccpartigtl  48474  iccpartgt  48478  icceuelpartlem  48486  fargshiftf1  48492  ichnreuop  48523  ichreuopeq  48524  elsprel  48526  sprsymrelfo  48548  prproropf1olem4  48557  paireqne  48562  sbcpr  48572  reupr  48573  goldbachth  48601  fmtnoprmfac1  48619  fmtnoprmfac2  48621  prmdvdsfmtnof1lem2  48639  lighneallem2  48660  lighneallem4  48664  requad2  48690  even3prm2  48786  fpprwpprb  48807  gbegt5  48828  sbgoldbwt  48844  sbgoldbm  48851  nnsum3primesgbe  48859  wtgoldbnnsum4prm  48869  bgoldbnnsum3prm  48871  bgoldbtbndlem2  48873  bgoldbtbndlem3  48874  bgoldbtbndlem4  48875  bgoldbtbnd  48876  isubgredg  48933  grimuhgr  48954  clnbgrgrim  49001  grtriprop  49008  cycl3grtrilem  49013  cycl3grtri  49014  gpgusgralem  49123  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgcubic  49146  gpg5nbgr3star  49148  gpgprismgr4cycllem3  49164  upgrwlkupwlk  49207  uspgropssxp  49211  uspgrsprfo  49215  isassintop  49276  lidldomn1  49297  2zlidl  49306  2zrngamgm  49311  2zrngmmgm  49318  rngccatidALTV  49338  rngcinvALTV  49342  rhmsubcALTVlem4  49350  funcringcsetcALTV2lem9  49364  ringccatidALTV  49372  srhmsubcALTV  49391  lmodvsmdi  49460  ply1mulgsumlem1  49467  ply1mulgsumlem2  49468  lincdifsn  49505  lincsumcl  49512  lincscmcl  49513  lincext3  49537  lindslinindsimp1  49538  lindslinindsimp2lem5  49543  snlindsntor  49552  lincresunit2  49559  lincresunit3lem2  49561  zgtp1leeq  49602  elbigo2  49633  fllog2  49649  digexp  49688  dig1  49689  nn0sumshdiglemA  49700  nn0sumshdiglemB  49701  1arymaptf1  49723  2arymaptf1  49734  rrxlinec  49817  eenglngeehlnm  49820  rrx2linest  49823  itsclc0yqsol  49845  itsclc0xyqsol  49849