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  1059  19.29r  1876  19.41v  1951  19.41  2243  nfsb4t  2504  mo4  2567  2euexv  2632  2euex  2642  raleqbidvvOLD  3307  gencl  3484  2gencl  3485  vtocl2ga  3535  vtocl2gaf  3536  vtocl3gaf  3538  vtocl3ga  3540  vtocl4g  3542  vtocl4ga  3543  rspccva  3577  2reurex  3720  2reu1  3849  rexdifi  4104  sseq0  4357  r19.2z  4454  falseral0OLD  4470  elelpwi  4566  preqsnd  4817  prproe  4863  ssuni  4890  disji2  5084  disjiun  5088  disjxiun  5097  trintss  5225  ssexg  5270  reusv2lem3  5347  propeqop  5463  otiunsndisj  5476  rexopabb  5484  pofun  5558  solin  5567  2optocl  5728  3optocl  5729  ssrelrn  5851  elrnmpt1  5917  resieq  5957  imadifssran  6117  reuop  6259  fnun  6614  fss  6686  fun  6704  fvelimab  6914  fvmptss  6962  fvn0ssdmfun  7028  fvcofneq  7047  fmptco  7084  funsndifnop  7106  fnressn  7113  fressnfv  7115  fmptsng  7124  fvtp2g  7155  fvtp3g  7156  tpres  7157  fnex  7173  funfvima3  7192  fvf1pr  7263  isores3  7291  tfisg  7806  dmfex  7857  opreuopreu  7988  releldmdifi  7999  funeldmdif  8002  el2mpocsbcl  8037  f1o2ndf1  8074  frxp  8078  fnse  8085  frxp2  8096  frxp3  8103  poseq  8110  ressuppssdif  8137  funsssuppss  8142  mpoxopxnop0  8167  reldmtpos  8186  frrlem8  8245  fpr2a  8254  smores  8294  tfrlem7  8324  tz7.48-2  8383  tz7.49  8386  oacl  8472  omcl  8473  oecl  8474  oarec  8499  oewordri  8530  oeworde  8531  oelim2  8533  oeoa  8535  oeoelem  8536  oeoe  8537  nnacl  8549  nnmcl  8550  nnecl  8551  nnmsucr  8563  naddoa  8640  brinxper  8675  2ecoptocl  8757  fsetprcnex  8811  undifixp  8884  xpf1o  9079  limensuc  9094  unfi  9107  en1eqsn  9187  ac6sfi  9196  frfi  9197  difinf  9223  imafiOLD  9228  f1dmvrnfibi  9253  f1vrnfibi  9254  suppeqfsuppbi  9294  elfiun  9345  dffi3  9346  infsupprpr  9421  xpwdomg  9502  infdiffi  9579  ttrclselem2  9647  epfrs  9652  frmin  9673  frr2  9684  rankxpsuc  9806  updjud  9858  tskwe  9874  infxpenlem  9935  fseqenlem1  9946  kmlem2  10074  nnadju  10120  cff1  10180  cflim2  10185  sornom  10199  infpssrlem4  10228  fin23lem26  10247  fin23lem30  10264  fin23lem34  10268  isf32lem11  10285  fin67  10317  isfin7-2  10318  fin1a2lem10  10331  axcc2lem  10358  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  iunfo  10461  tsk0  10686  gruina  10741  grur1a  10742  mulcanenq  10883  reclem2pr  10971  supsrlem  11034  supsr  11035  ax1rid  11084  negf1o  11579  mulgt1OLD  12012  lbreu  12104  nnindd  12177  nnaddcl  12180  nnmulcl  12181  nn0n0n1ge2b  12482  nn0indd  12601  fzind  12602  fnn0ind  12603  uzaddcl  12829  uzinfi  12853  nn01to3  12866  elpq  12900  xmulasslem2  13209  supxrunb1  13246  supxrunb2  13247  infmremnf  13271  infmrp1  13272  uzsubsubfz  13474  fzdif1  13533  elfz0ubfz0  13560  fz0fzdiffz0  13565  elfzmlbp  13567  fzofzim  13637  elfzom1elp1fzo  13660  ssfzo12bi  13689  fzoopth  13690  fzonfzoufzol  13699  elfznelfzob  13702  injresinjlem  13718  injresinj  13719  modaddmodup  13869  modfzo0difsn  13878  modsumfzodifsn  13879  addmodlteq  13881  om2uzlti  13885  fsequb  13910  ssnn0fi  13920  ser1const  13993  expcllem  14007  expeq0  14027  expmordi  14102  expnngt1  14176  faclbnd  14225  hashf1rn  14287  hashgadd  14312  hashunx  14321  hashnn0n0nn  14326  hashgt0elex  14336  hashss  14344  hashfzp1  14366  hashxp  14369  hashmap  14370  hashimarni  14376  seqcoll  14399  hash2exprb  14406  hashge2el2difr  14416  elss2prb  14423  hashdifsnp1  14441  fi1uzind  14442  brfi1indALT  14445  lswlgt0cl  14504  swrdnd  14590  swrdnnn0nd  14592  swrdnd0  14593  swrd0  14594  swrdsbslen  14600  swrdspsleq  14601  pfxsuff1eqwrdeq  14634  swrdswrdlem  14639  swrdswrd  14640  wrd2ind  14658  pfxccatin12lem2a  14662  swrdccatin2  14664  pfxccatin12lem2  14666  pfxccatin12lem3  14667  pfxccatin12  14668  pfxccat3  14669  swrdccat  14670  pfxccat3a  14673  swrdccat3blem  14674  repswswrd  14719  repswrevw  14722  cshwmodn  14730  cshwsublen  14731  cshwidxmod  14738  cshwidxmodr  14739  cshf1  14745  2cshw  14748  cshweqrep  14756  cshw1  14757  2cshwcshw  14760  cshwcshid  14762  cshwcsh2id  14763  wrdlen2i  14877  2swrd2eqwrdeq  14888  wwlktovfo  14893  relexpsucnnl  14965  rtrclreclem3  14995  rtrclreclem4  14996  relexpindlem  14998  r19.29uz  15286  caubnd  15294  sqreu  15296  climshft  15511  climub  15597  climserle  15598  sumss  15659  sumss2  15661  modfsummods  15728  o1fsum  15748  binom  15765  climcndslem1  15784  climcndslem2  15785  cvgrat  15818  clim2prod  15823  prodfn0  15829  prodfrec  15830  ntrivcvgfvn0  15834  fprodn0  15914  fprodmodd  15932  fprodefsum  16030  demoivreALT  16138  ruclem8  16174  dvdsaddre2b  16246  dvdsdivcl  16255  dvdsfac  16265  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  m1exp1  16315  nn0o  16322  pwp1fsum  16330  flodddiv4  16354  smu01lem  16424  dvdslegcd  16443  gcdneg  16461  dfgcd2  16485  seq1st  16510  alginv  16514  lcmf  16572  lcmftp  16575  lcmfunsnlem2lem2  16578  lcmfunsnlem  16580  lcmfun  16584  ncoprmgcdne1b  16589  coprmproddvdslem  16601  coprmproddvds  16602  cncongr1  16606  prmdvdsexp  16654  prmndvdsfaclt  16664  ncoprmlnprm  16667  fvprmselgcd1  16985  prmgaplem6  16996  prmgaplem7  16997  prmgaplem8  16998  cshwshashlem1  17035  setsstruct2  17113  setsstruct  17115  inveq  17710  catsubcat  17775  initoeu2lem0  17949  initoeu2lem1  17950  funcestrcsetclem8  18082  funcestrcsetclem9  18083  fthestrcsetc  18085  fullestrcsetc  18086  funcsetcestrclem9  18098  fthsetcestrc  18100  fullsetcestrc  18101  lubss  18448  lubel  18449  mgmpropd  18588  issstrmgm  18590  mgmb1mgm1  18592  sgrpidmnd  18676  frmdgsum  18799  smndex1mndlem  18846  mgm2nsgrplem3  18857  dfgrp2  18904  cyccom  19144  gaass  19238  gsumwrev  19307  symgextf1lem  19361  symgextf1  19362  fvcosymgeq  19370  gsmsymgreq  19373  symgfixelsi  19376  pmtrprfv3  19395  symggen  19411  pmtrprfval  19428  gsumzres  19850  gsumpr  19896  gsumzunsnd  19897  srgmulgass  20164  srgbinom  20178  0ringnnzr  20470  rnghmsscmap  20575  rnghmsubcsetclem2  20577  rngcinv  20582  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap  20604  rhmsubcsetclem2  20606  rhmsubcrngclem2  20612  funcringcsetc  20619  srhmsubc  20625  rhmsubclem4  20633  lmodvsmmulgdi  20860  lmodfopnelem1  20861  rmodislmodlem  20892  rngqiprngimfo  21268  cnfldmulg  21370  cnfldexp  21371  ofldchr  21543  psgndiflemB  21567  assamulgscm  21869  gsumply1subr  22186  gsummoncoe1  22264  pf1ind  22311  matmulcell  22401  mat1dimscm  22431  dmatmul  22453  dmatscmcl  22459  scmataddcl  22472  scmatsubcl  22473  scmatsgrp1  22478  mavmulsolcl  22507  ma1repveval  22527  1marepvmarrepid  22531  symgmatr01lem  22609  slesolvec  22635  cramerimplem2  22640  decpmatmullem  22727  pm2mpf1  22755  mp2pm2mplem4  22765  monmat2matmon  22780  chpscmat  22798  chpscmatgsumbin  22800  fvmptnn04ifb  22807  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  cpmadugsumlemF  22832  toprntopon  22881  clsss  23010  ntrss  23011  restntr  23138  cmpsublem  23355  cmpsub  23356  2ndcrest  23410  txindislem  23589  t0kq  23774  filufint  23876  fbflim2  23933  flftg  23952  alexsubALTlem4  24006  cnextfvval  24021  ustuqtop4  24200  xmettri2  24296  mettri  24308  metss  24464  tngngp3  24612  clmvscom  25058  lmmbr  25226  caublcls  25277  lmcau  25281  ovolunlem1a  25465  nulmbl2  25505  voliunlem1  25519  iunmbl  25522  volsup  25525  dvlip  25966  dvfsumle  25994  dvfsumleOLD  25995  degltlem1  26045  ply1divex  26110  plyco  26214  dgrnznn  26220  dvnply2  26263  plydivex  26273  aannenlem2  26305  aaliou3lem2  26319  ulmcau  26372  zabsle1  27275  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  gausslemma2dlem3  27347  gausslemma2dlem4  27348  2lgslem1a1  27368  2sqnn0  27417  2sqreulem1  27425  2sqreunnlem1  27428  dchrisumlem1  27468  dchrisumlem2  27469  dchrisumlem3  27470  qabvle  27604  ostthlem2  27607  ostth2lem2  27613  nosupbnd1lem5  27692  noinfbnd1lem5  27707  nocvxminlem  27762  lesrec  27807  madebdaylemold  27906  mulsuniflem  28157  precsexlem6  28220  precsexlem7  28221  precsexlem8  28222  precsexlem9  28223  abssge0  28253  noseqind  28300  om2noseqlt  28307  om2noseqrdg  28312  n0addscl  28352  n0mulscl  28353  onsfi  28364  oldfib  28385  expscllem  28438  pw2cut2  28470  z12zsodd  28490  tgjustr  28558  axeuclidlem  29047  incistruhgr  29164  umgredgprv  29192  umgrpredgv  29225  usgredgprvALT  29280  uhgr2edg  29293  usgredg2vlem2  29311  lfuhgr1v0e  29339  subgrfun  29366  umgrres1lem  29395  upgrres1  29398  fusgrfis  29415  uhgrnbgr0nb  29439  nbgr1vtx  29443  nb3grprlem1  29465  uvtx01vtx  29482  fusgrn0degnn0  29585  vtxdginducedm1lem4  29628  finsumvtxdg2size  29636  wlkl1loop  29723  wlkres  29754  lfgrwlknloop  29773  pthdadjvtx  29813  dfpth2  29814  upgr2pthnlp  29817  upgrwlkdvdelem  29821  upgrwlkdvde  29822  uhgrwkspthlem2  29839  usgr2trlspth  29846  usgr2pth  29849  pthdlem2lem  29852  cyclnumvtx  29885  lfgrn1cycl  29890  uspgrn2crct  29893  crctcshwlkn0lem3  29897  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  iswspthsnon  29941  wlkiswwlks1  29952  wlklnwwlkln1  29953  wlkiswwlks2  29960  wlkiswwlksupgr2  29962  wlklnwwlkln2lem  29967  wlknwwlksnbij  29973  wwlksnred  29977  wwlksnext  29978  wwlksnredwwlkn  29980  wwlksnredwwlkn0  29981  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextsurj  29985  wspthsnonn0vne  30002  wspn0  30009  wwlks2onv  30038  elwwlks2  30054  elwspths2spth  30055  rusgrnumwwlk  30063  clwwlkccatlem  30076  clwlkclwwlklem2a1  30079  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  clwlkclwwlkf1lem3  30093  clwwisshclwwslem  30101  clwwisshclwwsn  30103  erclwwlktr  30109  isclwwlknx  30123  clwwlkinwwlk  30127  clwwlkel  30133  clwwlkf  30134  clwwlkf1  30136  clwwlkfo  30137  clwwlkext2edg  30143  wwlksext2clwwlk  30144  wwlksubclwwlk  30145  clwwlknscsh  30149  erclwwlkntr  30158  eleclclwwlkn  30163  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  clwwlknon0  30180  clwwlknonel  30182  clwwlknon1  30184  clwwlknonwwlknonb  30193  clwwlknonex2lem2  30195  clwwlknun  30199  clwwlkvbij  30200  upgr3v3e3cycl  30267  uhgr3cyclex  30269  upgr4cycl4dv4e  30272  eulerpath  30328  eucrctshift  30330  eucrct2eupth  30332  1to2vfriswmgr  30366  1to3vfriswmgr  30367  3cyclfrgrrn1  30372  4cycl2vnunb  30377  frgrwopreglem2  30400  frgrwopreglem3  30401  frgrwopreglem5ALT  30409  fusgr2wsp2nb  30421  2clwwlk2clwwlklem  30433  2clwwlk2clwwlk  30437  numclwwlk1lem2f1  30444  numclwwlk1lem2fo  30445  numclwwlk1  30448  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  numclwlk1  30458  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  numclwwlk5  30475  frgrreg  30481  frgrregord013  30482  friendship  30486  nsnlplig  30569  nsnlpligALT  30570  isgrpo  30585  vcdi  30653  vcdir  30654  vcass  30655  nmosetre  30852  hlim2  31280  shscli  31405  chintcli  31419  dfch2  31495  spansncvi  31740  nmopsetretALT  31951  nmfnsetre  31965  lnopl  32002  lnfnl  32019  pjss2coi  32252  pjorthcoi  32257  pjscji  32258  pjssdif2i  32262  pjclem4a  32286  pj3lem1  32294  strlem5  32343  hstrlem5  32351  cvmdi  32412  mdslmd3i  32420  atcv1  32468  atcvat4i  32485  cdj3lem2a  32524  cdj3lem3a  32527  opreu2reuALT  32563  iuninc  32647  disji2f  32664  disjif2  32668  fmptcof2  32747  xrsmulgzz  33102  1arithufdlem3  33639  esumfzf  34247  issgon  34301  voliune  34407  volfiniune  34408  rrvsum  34632  bnj228  34912  bnj1294  34993  bnj229  35060  bnj607  35092  bnj908  35107  bnj953  35115  bnj1118  35160  bnj1174  35179  bnj1388  35209  funen1cnv  35265  rankfilimbi  35278  r1filimi  35280  trssfir1om  35289  trssfir1omregs  35314  acycgrsubgr  35374  cvmliftlem15  35514  satfsschain  35580  satfdm  35585  satf0op  35593  fmla0xp  35599  gonarlem  35610  goalrlem  35612  satffunlem1lem1  35618  satffunlem2lem1  35620  dmopab3rexdif  35621  satefvfmla0  35634  prv1n  35647  iprodefisumlem  35956  faclimlem1  35959  dfon2lem6  36002  idinside  36300  onsucconni  36653  bj-cbvew  36885  axc11n11r  36928  bj-brrelex12ALT  37315  bj-snmoore  37366  bj-finsumval0  37540  exlimim  37597  exellim  37599  icoreclin  37612  difunieq  37629  fvineqsneq  37667  pibt2  37672  wl-spae  37776  wl-aleq  37790  fin2so  37858  matunitlindf  37869  poimirlem4  37875  poimirlem26  37897  itg2addnclem  37922  upixp  37980  welb  37987  sdclem2  37993  metf1o  38006  sstotbnd3  38027  isbndx  38033  ismtycnv  38053  heiborlem4  38065  bfplem1  38073  opidonOLD  38103  grpomndo  38126  eldisjdmqsim2  39067  ax12eq  39317  ax12el  39318  cvrat4  39819  nn0addcom  42832  nn0mulcom  42836  mzpexpmpt  43102  diophren  43170  rmxypos  43304  jm2.17a  43317  jm2.17b  43318  rmygeid  43321  jm2.18  43345  jm2.25  43356  jm2.15nn0  43360  jm2.16nn0  43361  pwslnm  43451  isnumbasgrplem1  43458  dgraalem  43502  onuniintrab  43583  onsupuni  43586  onsupcl3  43590  naddonnn  43752  naddwordnexlem2  43755  relexpiidm  44060  relexpmulnn  44065  relexpmulg  44066  relexp01min  44069  relexp0a  44072  relexpxpmin  44073  clsk1indlem3  44399  grucollcld  44616  dvgrat  44668  radcnvrat  44670  sspwimpcf  45275  sspwimpcfVD  45276  e2ebindALT  45284  trfr  45318  et-sqrtnegnre  47231  fsetprcnexALT  47422  eu2ndop1stv  47485  afvfv0bi  47512  afveu  47513  afvres  47532  aovmpt4g  47561  ndmaovass  47566  ndmaovdistr  47567  afv2orxorb  47588  afv2eu  47598  imarnf1pr  47642  nltle2tri  47673  fzopredsuc  47683  subsubelfzo0  47686  2ffzoeq  47687  2tceilhalfelfzo1  47692  m1modmmod  47718  smonoord  47731  elsetpreimafvssdm  47746  iccpartres  47778  iccpartiltu  47782  iccpartigtl  47783  iccpartgt  47787  icceuelpartlem  47795  fargshiftf1  47801  ichnreuop  47832  ichreuopeq  47833  elsprel  47835  sprsymrelfo  47857  prproropf1olem4  47866  paireqne  47871  sbcpr  47881  reupr  47882  goldbachth  47907  fmtnoprmfac1  47925  fmtnoprmfac2  47927  prmdvdsfmtnof1lem2  47945  lighneallem2  47966  lighneallem4  47970  requad2  47983  even3prm2  48079  fpprwpprb  48100  gbegt5  48121  sbgoldbwt  48137  sbgoldbm  48144  nnsum3primesgbe  48152  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbndlem4  48168  bgoldbtbnd  48169  isubgredg  48226  grimuhgr  48247  clnbgrgrim  48294  grtriprop  48301  cycl3grtrilem  48306  cycl3grtri  48307  gpgusgralem  48416  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgcubic  48439  gpg5nbgr3star  48441  gpgprismgr4cycllem3  48457  upgrwlkupwlk  48500  uspgropssxp  48504  uspgrsprfo  48508  isassintop  48570  lidldomn1  48591  2zlidl  48600  2zrngamgm  48605  2zrngmmgm  48612  rngccatidALTV  48632  rngcinvALTV  48636  rhmsubcALTVlem4  48644  funcringcsetcALTV2lem9  48658  ringccatidALTV  48666  srhmsubcALTV  48685  lmodvsmdi  48739  ply1mulgsumlem1  48746  ply1mulgsumlem2  48747  lincdifsn  48784  lincsumcl  48791  lincscmcl  48792  lincext3  48816  lindslinindsimp1  48817  lindslinindsimp2lem5  48822  snlindsntor  48831  lincresunit2  48838  lincresunit3lem2  48840  zgtp1leeq  48881  elbigo2  48912  fllog2  48928  digexp  48967  dig1  48968  nn0sumshdiglemA  48979  nn0sumshdiglemB  48980  1arymaptf1  49002  2arymaptf1  49013  rrxlinec  49096  eenglngeehlnm  49099  rrx2linest  49102  itsclc0yqsol  49124  itsclc0xyqsol  49128