Theorem expcom 451

Description: Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
ex.1	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
expcom	|- ( ps -> ( ph -> ch ) )

Proof of Theorem expcom

Step	Hyp	Ref	Expression
1		ex.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 450	. 2 |- ( ph -> ( ps -> ch ) )
3	2	com12 32	1 |- ( ps -> ( ph -> ch ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  ancoms  469  syldan  487  sylan  488  4casesdan  991  dedlema  1002  dedlemb  1003  cbval2  2279  cbvaldva  2281  2moswap  2547  2eu2  2554  pm2.61ne  2879  nelelne  2892  r19.21be  2933  rspcebdv  3314  minel  4033  uneqdifeq  4057  uneqdifeqOLD  4058  raltpd  4315  ssunsn2  4359  ssuni  4459  ssuniOLD  4460  uniss2  4470  elpwuni  4616  disjord  4641  elssabg  4819  elpw2g  4827  oteqex  4964  otsndisj  4979  otiunsndisj  4980  epelg  5030  wereu  5110  relop  5272  riinint  5382  sotri3  5526  unixpid  5670  ordtr2  5768  ordsssuc2  5814  funopg  5922  fun  6066  tz6.12c  6213  fvmptnf  6302  fvn0ssdmfun  6350  eldmrexrnb  6366  fmptco  6396  funopsn  6413  fnressn  6425  fressnfv  6427  fvtp2g  6464  fvtp3g  6465  fconst2g  6468  fntpb  6473  f1dom3el3dif  6526  isores3  6585  isoselem  6591  oprabv  6703  eloprabga  6747  sorpsscmpl  6948  difex2  6969  ordpwsuc  7015  ordsucun  7025  limuni3  7052  ordom  7074  fo1stres  7192  poxp  7289  soxp  7290  suppimacnv  7306  frnsuppeq  7307  funsssuppss  7321  brtpos2  7358  wfrlem12  7426  onnseq  7441  smores  7449  smofvon2  7453  tfrlem1  7472  oacl  7615  omcl  7616  oecl  7617  oawordri  7630  oalimcl  7640  oaass  7641  oarec  7642  omwordri  7652  omeulem1  7662  omeulem2  7663  oeordi  7667  oeworde  7673  oeoelem  7678  nnacl  7691  nnmcl  7692  nnecl  7693  nnacom  7697  nnaass  7702  nnmsucr  7705  nnmordi  7711  omabs  7727  iiner  7819  elpmg  7873  pmss12g  7884  mapsn  7899  f1domg  7975  ssdomg  8001  domtriord  8106  php  8144  php3  8146  1sdom  8163  fisseneq  8171  isinf  8173  ssnnfi  8179  dif1en  8193  findcard3  8203  frfi  8205  unfi  8227  difinf  8230  fnfi  8238  iunfi  8254  fsuppunfi  8295  fsuppres  8300  frnfsuppbi  8304  elfi2  8320  marypha1lem  8339  marypha1  8340  oiexg  8440  wemapso2  8458  harword  8470  brwdom  8472  unxpwdom  8494  en3lplem1  8511  inf3lemd  8524  inf3lem5  8529  cantnfval2  8566  cantnfle  8568  cantnflt  8569  cnfcom  8597  tcmin  8617  r1sdom  8637  rankxplim3  8744  cardidm  8785  cardmin2  8824  infxpenlem  8836  fseqenlem1  8847  numacn  8872  alephordi  8897  iscard3  8916  alephinit  8918  carduniima  8919  iunfictbso  8937  dfac5  8951  dfac12lem3  8967  pwsdompw  9026  pwcdadom  9038  cflim2  9085  cfslb2n  9090  cofsmo  9091  cfsmolem  9092  cfcoflem  9094  alephsing  9098  infpssALT  9135  fin23lem34  9168  isf32lem2  9176  isf32lem10  9184  isf32lem12  9186  isfin1-2  9207  hsmexlem4  9251  axcc2lem  9258  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  ac6num  9301  ac6s  9306  zorn2lem7  9324  ttukeylem5  9335  imadomg  9356  iundom2g  9362  ondomon  9385  ficard  9387  konigthlem  9390  alephreg  9404  pwcfsdom  9405  cfpwsdom  9406  axregndlem1  9424  axregnd  9426  pwfseqlem3  9482  pwxpndom2  9487  pwxpndom  9488  pwcdandom  9489  inawinalem  9511  gchina  9521  wuncval2  9569  tsk0  9585  tskxpss  9594  inatsk  9600  tskuni  9605  gruina  9640  grothac  9652  addclpi  9714  addnidpi  9723  nqereu  9751  mulcanenq  9782  genpnnp  9827  nqpr  9836  prlem934  9855  reclem2pr  9870  suplem1pr  9874  supsrlem  9932  axpre-sup  9990  1re  10039  dedekindle  10201  00id  10211  receu  10672  sup3  10980  infrelb  11008  peano5nni  11023  nnaddcl  11042  zrevaddcl  11422  nzadd  11425  zdiv  11447  nneo  11461  zeo2  11464  nn0indd  11474  fzind  11475  fnn0ind  11476  uzwo  11751  lbzbi  11776  nn01to3  11781  qrevaddcl  11810  irradd  11812  irrmul  11813  ltsubrp  11866  ltaddrp  11867  xnn0xaddcl  12066  xnn0xadd0  12077  icoshft  12294  fzen  12358  elfzm11  12411  uzsplit  12412  elfzoext  12524  elfzom1elp1fzo  12534  injresinjlem  12588  injresinj  12589  modifeq2int  12732  modsumfzodifsn  12743  om2uzlti  12749  ssnn0fi  12784  fsuppmapnn0fiub0  12793  mptnn0fsuppr  12799  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqcaopr3  12836  seqf1olem2a  12839  seqf1o  12842  seqid2  12847  seqhomo  12848  ser1const  12857  expadd  12902  expmul  12905  leexp1a  12919  faccl  13070  facdiv  13074  faclbnd  13077  faclbnd4lem4  13083  faclbnd6  13086  hasheqf1oi  13140  hasheqf1oiOLD  13141  hashf1rnOLD  13143  hashgadd  13166  hashinfxadd  13174  hashunx  13175  hashunsng  13181  elprchashprn2  13184  hashss  13197  hash1snb  13207  hashmap  13222  hashf1lem2  13240  hashf1  13241  seqcoll  13248  hashle2pr  13259  hashdmpropge2  13265  hashge3el3dif  13268  hash1to3  13273  fundmge2nop0  13274  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  sswrd  13313  swrdnd2  13433  swrdswrdlem  13459  swrdswrd  13460  wrd2ind  13477  swrdccatin1  13483  swrdccatin2  13487  swrdccatin12lem2  13489  swrdccat3  13492  repsdf2  13525  repswswrd  13531  cshw0  13540  cshwcl  13544  cshwlen  13545  cshf1  13556  swrdco  13583  relexpsucnnl  13772  rtrclreclem3  13800  rtrclreclem4  13801  relexpindlem  13803  rtrclind  13805  shftlem  13808  caubnd  14098  rlimcld2  14309  o1dif  14360  climub  14392  climserle  14393  iseraltlem2  14413  sumss  14455  fsumzcl2  14469  fsummsnunz  14483  fsumsplitsnun  14484  fsummsnunzOLD  14485  fsumsplitsnunOLD  14486  fsum2d  14502  modfsummods  14525  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  cvgrat  14615  clim2prod  14620  prodfn0  14626  prodfrec  14627  ntrivcvg  14629  prodmo  14666  fprodss  14678  fprodabs  14704  fprodn0  14709  fprod2d  14711  fprodefsum  14825  ruclem8  14966  ruclem9  14967  dvds2ln  15014  dvdsaddre2b  15029  dvdslelem  15031  dvdsdivcl  15038  alzdvds  15042  mod2eq1n2dvds  15071  oddnn02np1  15072  nn0o1gt2  15097  nno  15098  sumeven  15110  sumodd  15111  pwp1fsum  15114  ndvdsadd  15134  bitsinv1  15164  sadcadd  15180  sadadd2  15182  saddisjlem  15186  smuval2  15204  smupvallem  15205  smu01lem  15207  smupval  15210  smueqlem  15212  smumullem  15214  gcddiv  15268  gcdmultiple  15269  rplpwr  15276  nn0seqcvgd  15283  seq1st  15284  alginv  15288  algcvga  15292  algfx  15293  absprodnn  15331  isprm2  15395  isprm3  15396  prmind2  15398  maxprmfct  15421  prmdvdsexp  15427  pcmpt  15596  prmreclem4  15623  vdwmc2  15683  vdwlem10  15694  ramub2  15718  ramcl  15733  prmgaplem5  15759  prmgaplem8  15762  cshwshashlem1  15802  cshwshashlem3  15804  setsn0fun  15895  imasleval  16201  divsfval  16207  mreexexlem4d  16307  isssc  16480  initoeu1  16661  termoeu1  16668  istos  17035  mgmcl  17245  frmdgsum  17399  dfgrp3lem  17513  mhmmulg  17583  resghm2b  17678  gsumwrev  17796  elsymgbas  17802  symgextf1  17841  gsmsymgreqlem2  17851  gsmsymgreq  17852  odlem1  17954  odcl2  17982  gexlem1  17994  sylow1lem1  18013  efgi2  18138  efginvrel2  18140  efgsrel  18147  cyggexb  18300  gsummulglem  18341  gsumzunsnd  18355  gsum2dlem2  18370  telgsums  18390  dmdprd  18397  dprdw  18409  ablfac1eulem  18471  srgpcomp  18532  lmodfopnelem1  18899  rmodislmodlem  18930  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  cply1mul  19664  coe1fzgsumdlem  19671  gsummoncoe1  19674  pf1ind  19719  evl1gsumdlem  19720  cnfldmulg  19778  cnfldexp  19779  obslbs  20074  mat1dimcrng  20283  ma1repveval  20377  mulmarep1gsum2  20380  gsummatr01lem3  20463  cramerlem3  20495  decpmatmulsumfsupp  20578  mp2pm2mplem4  20614  pm2mpmhmlem1  20623  fvmptnn04if  20654  cayhamlem1  20671  fctop  20808  mretopd  20896  restopnb  20979  restdis  20982  tgcnp  21057  cncls2  21077  cncls  21078  cnntr  21079  cnsscnp  21083  cmpsub  21203  2ndcsep  21262  1stcelcls  21264  lfinpfin  21327  locfincmp  21329  comppfsc  21335  txcn  21429  txlm  21451  xkohaus  21456  qtopres  21501  haushmphlem  21590  cmphmph  21591  connhmph  21592  reghmph  21596  nrmhmph  21597  ptcmpfi  21616  reghaus  21628  fbssfi  21641  fbun  21644  fbfinnfr  21645  isfildlem  21661  fgcl  21682  cfinfil  21697  supfil  21699  ufinffr  21733  fin1aufil  21736  cnpflf  21805  alexsubALTlem3  21853  alexsubALT  21855  cnextfvval  21869  cnextcn  21871  tmdmulg  21896  tmdgsum  21899  tgphaus  21920  tgpt1  21921  mettri  22157  imasdsf1olem  22178  blssexps  22231  blssex  22232  mopni3  22299  metss  22313  psmetutop  22372  dscmet  22377  tngngp3  22460  rectbntr0  22635  metnrmlem1a  22661  fsumcn  22673  lmmbr  23056  caubl  23106  caublcls  23107  bcthlem5  23125  bcth3  23128  ovolunlem1a  23264  ovoliunnul  23275  ovolicc2lem3  23287  finiunmbl  23312  voliunlem1  23318  volsuplem  23323  volsup  23324  dyadmax  23366  itgfsum  23593  dvnadd  23692  dvnres  23694  cpnord  23698  dvnfre  23715  dvmptfsum  23738  dvlip  23756  fta1g  23927  plyco  23997  dgrcolem1  24029  dgrco  24031  dvnply2  24042  plydivex  24052  plyexmo  24068  aannenlem1  24083  aaliou3lem2  24098  dvntaylp  24125  taylthlem1  24127  ulmval  24134  cxpmul2  24435  scvxcvx  24712  jensenlem2  24714  jensen  24715  ppiub  24929  bcmono  25002  bpos1lem  25007  bposlem5  25013  gausslemma2dlem6  25097  lgsquad2lem2  25110  2lgslem3  25129  2lgs  25132  dchrisumlem1  25178  dchrisum0flb  25199  pntpbnd1  25275  pntlemf  25294  qabvle  25314  qabvexp  25315  ostthlem2  25317  ostth2lem2  25323  axeuclidlem  25842  axcontlem12  25855  umgrnloopv  26001  uhgredgrnv  26025  edglnl  26038  numedglnl  26039  usgruspgrb  26076  usgrnloopvALT  26093  usgredg2vlem2  26118  subupgr  26179  nbumgr  26243  uhgrnbgr0nb  26250  nbgr0vtxlem  26251  edgusgrnbfin  26275  nb3grprlem2  26283  uvtxanbgrvtx  26293  cplgrop  26333  cusgrfi  26354  fusgrmaxsize  26360  fusgrn0degnn0  26395  ewlkprop  26499  uspgr2wlkeq  26542  g0wlk0  26548  wlkreslem  26566  wlkres  26567  lfgriswlk  26585  upgrwlkdvde  26633  spthonepeq  26648  uhgrwkspth  26651  usgr2trlncl  26656  usgr2trlspth  26657  cyclnspth  26695  crctcshwlkn0lem3  26704  wwlksn  26729  wspthneq1eq2  26745  wwlksm1edg  26767  wwlksnred  26787  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextproplem3  26806  wspthsnonn0vne  26813  rusgrnumwwlk  26870  clwwlksn  26881  clwlkclwwlklem2  26901  clwlkclwwlklem3  26902  umgrclwwlksge2  26912  wwlksubclwwlks  26925  clwwisshclwws  26928  clwwisshclwwsn  26929  clwlksfclwwlk  26962  upgr3v3e3cycl  27040  uhgr3cyclex  27042  upgr4cycl4dv4e  27045  eupthseg  27066  upgreupthseg  27069  eupth2lem3lem4  27091  eupth2lem3lem7  27094  eupth2  27099  eulerpath  27101  nfrgr2v  27136  frgr3vlem1  27137  3vfriswmgr  27142  1to2vfriswmgr  27143  1to3vfriswmgr  27144  3cyclfrgrrn1  27149  3cyclfrgrrn  27150  3cyclfrgrrn2  27151  4cycl2vnunb  27154  frgrncvvdeqlem2  27164  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  frgrwopreglem4a  27174  frgrwopreglem5lem  27184  frgrwopreglem5ALT  27186  frgrregorufr0  27188  frgr2wwlk1  27193  frgr2wwlkeqm  27195  fusgr2wsp2nb  27198  2wspmdisj  27201  frrusgrord  27205  numclwwlkovf2exlem2  27212  numclwlk1lem2foa  27224  numclwlk1lem2f1  27227  frgrreggt1  27251  friendshipgt3  27256  hlim2  28049  elnlfn  28787  stle0i  29098  hstrbi  29125  spansncv2  29152  h1da  29208  fmptcof2  29457  nnindd  29566  xreceu  29630  tpr2rico  29958  hasheuni  30147  ismeas  30262  sseqp1  30457  rrvsum  30516  dstfrvunirn  30536  sgn3da  30603  bnj607  30986  bnj1145  31061  bnj1204  31080  subfacp1lem6  31167  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem12  31296  cvmlift3lem4  31304  mrsubvrs  31419  climuzcnv  31565  iprodefisumlem  31626  fprb  31669  dfon2lem9  31696  trpredtr  31730  trpredmintr  31731  dftrpred3g  31733  trpredrec  31738  soseq  31751  frrlem11  31792  sltval2  31809  sltsolem1  31826  linethru  32260  elhf2  32282  finminlem  32312  fnessref  32352  neibastop2lem  32355  fnemeet2  32362  nndivsub  32456  bj-cbval2v  32737  bj-xpnzex  32946  bj-intss  33053  mptsnunlem  33185  dissneqlem  33187  topdifinffinlem  33195  iooelexlt  33210  wl-exeq  33321  wl-ax11-lem3  33364  matunitlindflem1  33405  poimirlem22  33431  poimirlem26  33435  poimirlem28  33437  poimirlem29  33438  poimirlem32  33441  heicant  33444  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  cover2  33508  upixp  33524  sdclem2  33538  fdc  33541  seqpo  33543  metf1o  33551  mettrifi  33553  sstotbnd3  33575  heibor1lem  33608  heiborlem5  33614  heibor  33620  bfplem1  33621  elghomlem2OLD  33685  grpokerinj  33692  isrngo  33696  rngodm1dm2  33731  ispridl2  33837  exlimddvf  33926  lssatle  34302  4atexlemex4  35359  mzpsubst  37311  jm2.18  37555  wepwsolem  37612  iunrelexp0  37994  relexpmulg  38002  cnvtrclfv  38016  clsk1indlem3  38341  dvgrat  38511  radcnvrat  38513  sbcoreleleqVD  39095  csbxpgVD  39130  sineq0ALT  39173  islptre  39851  iblspltprt  40189  stoweidlem2  40219  stoweidlem17  40234  stoweidlem21  40238  2reu2  41187  afveu  41233  funbrafv  41238  ndmaovass  41286  funop1  41302  nltle2tri  41323  2elfz2melfz  41328  fzoopth  41337  smonoord  41341  fsummsndifre  41342  fsumsplitsndif  41343  fsummmodsndifre  41344  fsummmodsnunz  41345  iccpartimp  41353  iccpartiltu  41358  iccpartigtl  41359  iccpartleu  41364  iccpartgel  41365  iccpartrn  41366  iccpartiun  41370  icceuelpart  41372  iccpartnel  41374  fargshiftf  41376  fargshiftf1  41377  pfxccatin12lem2  41424  pfxccat3  41426  fmtnoinf  41448  odz2prm2pw  41475  lighneallem4  41527  lighneal  41528  evensumeven  41616  even3prm2  41628  gbowgt5  41650  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbnnsum3prm  41692  bgoldbtbndlem2  41694  bgoldbtbndlem4  41696  bgoldbtbnd  41697  elsprel  41725  prsprel  41737  sprsymrelfo  41747  clcllaw  41827  nrhmzr  41873  rnghmmul  41900  rngccatidALTV  41989  ringccatidALTV  42052  nzerooringczr  42072  scmsuppss  42153  gsumlsscl  42164  ply1mulgsumlem2  42175  lincvalsc0  42210  linc0scn0  42212  lincdifsn  42213  linc1  42214  lincellss  42215  lincsum  42218  lincscm  42219  lincsumcl  42220  lcoss  42225  lincext3  42245  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lindsrng01  42257  snlindsntor  42260  lincresunit3lem2  42269  lincresunit3  42270  islindeps2  42272  blengt1fldiv2p1  42387