Theorem com23 32

Description: Commutation of antecedents. Swap 2nd and 3rd.

Hypothesis

Ref	Expression
com3.1	|- (ph -> (ps -> (ch -> th)))

Assertion

Ref	Expression
com23	|- (ph -> (ch -> (ps -> th)))

Proof of Theorem com23

Step	Hyp	Ref	Expression
1		com3.1	. 2 |- (ph -> (ps -> (ch -> th)))
2		pm2.04 30	. 2 |- ((ps -> (ch -> th)) -> (ch -> (ps -> th)))
3	1, 2	syl 10	1 |- (ph -> (ch -> (ps -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  com13 33  com3l 34  com24 37  mpii 45  pm2.86 69  impt 139  ancom2s 490  prth 559  elimant 688  pclem6 746  dedlem0b 766  dedlemb 768  dn1 779  3com23 845  meredith 931  a4imt 1195  cbv1 1199  sbied 1232  sbequi 1265  ax11indn 1405  eqrdav 1517  r19.21adva 1765  r19.21advva 1768  ralcom2 1822  reu3 1977  sbciegft 2007  reuss2 2327  reupick 2331  ssiun 2660  pwssun 2905  wefrc 2970  ordelord 2997  tz7.7 3001  onfr 3014  ordtr2 3019  onmindif 3061  unizlim 3086  ralxfrd 3120  limsssuc 3204  tfinds 3212  tfindsg 3213  limomss 3224  findsg 3245  funssres 3657  funcnvuni 3669  fv3 3844  funfvima2 3967  isoini 4014  f1oweALT 4020  onfununi 4209  onopriun 4211  tfrlem1 4212  tz7.49 4260  abianfp 4263  oarec 4332  omordi 4333  omlimcl 4345  omass 4347  oeordi 4350  oeordsuc 4357  nnmordi 4386  nnaordex 4389  nnawordex 4390  oaabs 4392  omsmolem 4396  eceqopreq 4454  th3qlem1 4455  en3d 4542  xpdom2 4583  ac6sfi 4591  sdomen2 4627  mapenlem2 4637  pssnn 4681  suc11reg 4750  inf3lem2 4759  inf3lem5 4762  noinfep 4786  trcl 4791  zfregs 4793  aceq5lem5 4885  zorn2lem4 4937  zorn2lem6 4939  zorn2lem7 4940  fodom 4944  uniimadom 4956  unxpdomlem 4993  alephordi 5024  ltbtwnpq 5238  genpcd 5263  psslinpr 5289  prlem934 5293  ltaddpr 5294  ltexprlem3 5298  ltexprlem6 5301  ltexprlem7 5302  ltapr 5305  prlem936b 5308  prlem936 5309  suplem1pr 5315  suppsr2 5377  suppsr3 5378  ltletr 5678  xrltletr 5717  divmul 5859  divne0 5875  lemul12a 5988  divgt0 5999  divge0 6000  nnsubi 6102  rpneg 6211  lbreu 6213  sup2 6219  infmrcl 6237  bndndx 6241  xrub 6248  supxrunb2 6258  elnnz 6313  btwnnz 6363  uzindOLD 6379  uzwo4OLD 6381  uzwo5OLD 6382  zindd 6386  zmax 6392  zbtwnre 6393  irradd 6416  irrmul 6417  qbtwnre 6418  icounlem 6539  ioojoin 6543  uzwo 6582  uzwoOLD 6583  fzopth 6632  fzrevral 6650  ser1add2i 6703  ser1addi 6704  le2sq2 6829  sqlecan 6838  sq01 6848  expnlbnd2 6854  absrpcl 7057  cau4ii 7121  cau5i 7122  caubndi 7129  facdiv 7145  facwordi 7147  faclbnd 7148  bccl2 7174  clm3i 7282  2climnn 7305  2climnn0 7306  climshfti 7307  climaddlem3 7319  climmullem8 7330  climsqueeze 7343  climsqueeze2 7344  climsupi 7358  caucvglem4 7363  caucvglem6 7365  reccnv 7422  cvgratlem1ALT 7452  cvgratlem5 7459  fsum0diag3 7465  fsum0diag4 7466  xpnnen 7711  infpnlem1 7718  infxpidmlem11 7774  uniopn 7810  basgen2 7851  subtop 7858  clsval2 7895  neii1 7931  neii2 7932  cncnpi 7983  cncnp 7988  metge0 8029  metxp 8044  ssbl 8065  opnin 8079  metequiv 8091  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni 8105  metcni2 8106  lmnn 8146  metelcls 8176  metcnp4lem2 8180  metcnp4 8181  iscms2lem5 8204  lmcau 8207  cmsss 8208  bcthlem18 8227  bcthlem21 8230  bcthlem28 8237  isgrp2i 8293  grplactf1o 8339  vacnlem3 8584  nmoub3i 8690  blocnilem 8719  ipasslem5 8750  ubthlem5 8791  ubthlem14 8802  minvecex 8838  efifolem4 8997  efifolem5 8998  chsscmi 9388  ocin 9445  ocnel 9446  occli 9457  projlem26 9487  spansneleq 9769  spansnss 9770  elspansn4 9772  h1datomi 9780  osumlem6 9861  spansncvi 9875  nmopub2tALT 10113  nmfnleub2 10130  nmcopexlem6 10235  nmcfnexlem6 10264  nlelchi 10273  bra11 10321  hstel2 10427  cvnbtwn 10494  spansncv2 10501  dmdmd 10508  dmdbr3 10513  dmdbr4 10514  dmdbr5 10516  mdsl0 10518  mdexchi 10543  cvexchlem 10576  atcv1 10589  atomli 10591  atcvatlem 10594  atcvat2i 10596  irredi 10603  atcvat4i 10606  mdsymlem3 10614  mdsymlem4 10615  sumdmdii 10624  sumdmdlem 10627  cdj1i 10642  cdj3lem1 10643  ghomf1olem 10681  ee7.2a 10710  uninqs 10730  oooeqim2 10759  xrletr2 10790  prj1 10809  unpde2eg22 10826  fiiu2 10852  lteqtpos 10880  tostos 10883  on1el4 10963  uznzr 10967  truni1 10999  truni2 11000  truni3 11001  hmphtr 11037  qusp 11068  fillsb 11073  fipfil2 11077  oefil2 11079  neifil 11080  efilcp 11083  efilcp2 11087  cnfilca 11088  rcfpfillem2 11090  bwt2 11123  iintlem1 11155  mrdmcd 11249  imonclem 11268  ismonc 11269  cmpmon 11270  icmpmon 11271  iepiclem 11278  isepic 11279  idsubfun 11312  trer 11409  elicc3 11410  ccid 11412  ioodisj 11413  finminlem 11418  elfiun 11421  inficlALT 11424  finsschain 11425  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  omsubsuc2 11439  omsubsdomlem2 11441  omsubinit 11451  opncldf1 11454  clsint2 11466  opnnei 11469  cncls 11473  cnntr 11474  subcls 11481  subntr 11482  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  cnconn 11503  reconnlem1 11507  reconn 11512  topbasfne 11560  fnessref 11564  lfinpfin 11574  locfincomp 11575  comppfsc 11578  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  topmtcl 11586  fnemeet2 11590  ist1-2 11603  ist1-3 11604  fbssint 11626  fbunfip 11631  fgid 11637  fgfil 11638  fgmin 11639  fbfgss 11640  extbas1 11641  isufil2 11650  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  filufint 11659  ufinffr 11663  ufilen 11664  filcon 11665  flimopn 11679  limfilcf 11683  hausfillim 11685  cnpfillim 11686  elfilmap2 11691  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  flimfbas 11713  fclusnei 11719  fclusbas 11722  fcluscf 11724  flimfnfcls 11727  fcluscnp 11730  fcluscomp 11733  fclusfnei 11738  dirtr 11753  tailfb 11762  filnetlem1 11763  filnetlem5 11767  raleqfn 11790  morex 11804  cardennn 11832  dif1en 11833  dif1card 11835  findcard 11836  fimax 11837  fixp 11840  indexf 11847  inficl 11849  fzm1 11867  sdc 11877  seqpo 11878  blhalf 11911  mettrifi 11912  ishomeo2 11957  lmtlm 11969  tx1cn 11976  tx2cn 11977  sstotbnd 11992  totbndss 11993  totbndbnd 12000  heiborlem1 12011  heiborlem13 12023  heiborlem15 12025  heiborlem16 12026  heiborlem23 12033  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  heiborlem40 12050  heiborlem41 12051  isphtpc2 12102  phtpcer 12104

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain