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 141  ancom2s 487  prth 555  elimant 683  pclem6 740  dedlem0b 760  dedlemb 762  3com23 838  meredith 922  a4imt 1156  cbv1 1160  sbied 1193  sbequi 1226  ax11indn 1364  r19.21adva 1716  r19.21advva 1719  ralcom2 1773  reu3 1927  sbciegft 1955  reuss2 2271  reupick 2275  ssiun 2587  pwssun 2822  ralxfrd 2892  wefrc 2938  ordelord 2965  tz7.7 2968  onfr 2981  ordtr2 2997  onmindif 3055  unizlim 3108  limsssuc 3116  limomss 3132  findsg 3152  tfinds 3156  tfindsg 3157  funssres 3544  funcnvuni 3556  fv3 3724  funfvima2 3844  isoini 3891  f1oweALT 3897  tfrlem1 3902  tz7.49 3950  abianfp 3953  oarec 4186  omordi 4187  omlimcl 4199  omass 4201  oeordi 4204  oeordsuc 4211  nnmordi 4236  nnaordex 4239  nnawordex 4240  oaabs 4242  omsmolem 4246  eceqopreq 4303  th3qlem1 4304  en3d 4388  xpdom2 4428  sdomen2 4468  mapenlem2 4476  pssnn 4519  suc11reg 4585  inf3lem2 4594  inf3lem5 4597  noinfep 4620  trcl 4625  zfregs 4627  aceq5lem5 4719  zorn2lem4 4771  zorn2lem6 4773  zorn2lem7 4774  fodom 4778  uniimadom 4790  unxpdomlem 4823  alephordi 4854  ltbtwnpq 5064  genpcd 5089  psslinpr 5115  prlem934 5119  ltaddpr 5120  ltexprlem3 5124  ltexprlem6 5127  ltexprlem7 5128  ltapr 5131  prlem936b 5134  prlem936 5135  suplem1pr 5141  suppsr2 5203  suppsr3 5204  ltletrt 5505  xrltletrt 5544  divne0t 5700  lemul12it 5808  divgt0t 5817  divge0t 5818  nnsub 5911  lbreu 6000  sup2 6006  infmrcl 6024  bndndx 6028  xrub 6035  supxrunb2 6045  elnnz 6100  btwnnzt 6147  uzindOLD 6164  uzwo4OLD 6166  uzwo5OLD 6167  zmax 6176  zbtwnre 6177  qbtwnre 6224  ser1add2 6283  ser1add 6284  icounlem 6353  uzwo 6395  uzwoOLD 6396  fzoptht 6442  fzrevralt 6459  le2sqit 6571  sqlecant 6580  sq01t 6590  absrpclt 6798  cau4i 6863  cau5 6864  caubnd 6871  facdivt 6887  facwordit 6889  faclbnd 6890  bccl2t 6917  clm3 7025  2climnn 7047  2climnn0 7048  climshft 7049  climaddlem3 7060  climmullem8 7071  climsqueeze 7084  climsqueeze2 7085  climsup 7099  caucvglem4 7104  caucvglem6 7106  reccnv 7161  cvgratlem1ALT 7190  cvgratlem5 7197  fsum0diag3 7203  fsum0diag4 7204  xpnnen 7449  znnenlemOLD 7452  infpnlem1 7457  infxpidmlem11 7513  uniopnt 7548  basgen2t 7589  subtop 7596  clsval2 7635  neii1 7671  neii2 7672  cncnpi 7723  cncnp 7728  metge0 7771  metxp 7786  ssbl 7807  opnin 7821  metcnp 7839  metcnpi3 7844  metcnpi4 7845  metcni 7846  metcni2 7847  lmnn 7887  metelcls 7916  metcnp4lem2 7919  metcnp4 7920  iscms2lem5 7943  lmcau 7946  cmsss 7947  bcthlem18 7966  bcthlem21 7969  bcthlem28 7976  isgrp2i 8026  grplactf1o 8049  nmoub3i 8381  blocnilem 8408  ipasslem5 8438  ubthlem5 8477  ubthlem14 8486  minvecex 8522  efifolem4 8659  efifolem5 8660  chsscm 9051  ocin 9108  ocnelt 9109  occl 9120  projlem26 9150  spansneleq 9432  spansneleqOLD 9433  spansnsst 9434  elspansn4t 9436  h1datom 9444  osumlem6 9523  spansncv 9537  nmopub2tALT 9773  nmfnleub2t 9789  nmcopexlem6 9894  nmcfnexlem6 9923  nlelch 9932  bra11 9979  hstel2t 10084  cvnbtwnt 10151  spansncv2t 10158  dmdmdt 10165  dmdbr3 10170  dmdbr4 10171  mdsl0 10174  mdexch 10199  cvexchlem 10232  atcv1t 10244  atoml 10246  atcvatlem 10249  atcvat2 10251  irred 10258  atcvat4 10261  mdsymlem3 10269  mdsymlem4 10270  sumdmdi 10278  sumdmdlem 10281  cdj1 10294  cdj3lem1 10295  ghomf1olem 10330  ee7.2a 10361  uninqs 10378  oooeqim2 10407  fiiu2 10413  truni1 10422  hmphtr 10454  qusp 10466  fillsb 10471  fipfil2 10475  oefil2 10477  neifil 10478  efilcp 10481  efilcp2 10486  cnfilca 10487  iintlem1 10512  mrdmcd 10602  imonclem 10619  ismonc 10620  cmpmon 10621  icmpmon 10623

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

Copyright terms: Public domain