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 556  elimant 684  pclem6 741  dedlem0b 761  dedlemb 763  3com23 839  meredith 924  a4imt 1158  cbv1 1162  sbied 1195  sbequi 1228  ax11indn 1366  r19.21adva 1719  r19.21advva 1722  ralcom2 1776  reu3 1931  sbciegft 1959  reuss2 2275  reupick 2279  ssiun 2592  pwssun 2827  ralxfrd 2897  wefrc 2943  ordelord 2970  tz7.7 2973  onfr 2986  ordtr2 3002  onmindif 3060  unizlim 3113  limsssuc 3121  limomss 3137  findsg 3157  tfinds 3161  tfindsg 3162  funssres 3552  funcnvuni 3564  fv3 3733  funfvima2 3853  isoini 3900  f1oweALT 3906  tfrlem1 3911  tz7.49 3959  abianfp 3962  oarec 4196  omordi 4197  omlimcl 4209  omass 4211  oeordi 4214  oeordsuc 4221  nnmordi 4246  nnaordex 4249  nnawordex 4250  oaabs 4252  omsmolem 4256  eceqopreq 4313  th3qlem1 4314  en3d 4401  xpdom2 4442  sdomen2 4482  mapenlem2 4490  pssnn 4534  suc11reg 4605  inf3lem2 4614  inf3lem5 4617  noinfep 4640  trcl 4645  zfregs 4647  aceq5lem5 4739  zorn2lem4 4791  zorn2lem6 4793  zorn2lem7 4794  fodom 4798  uniimadom 4810  unxpdomlem 4843  alephordi 4874  ltbtwnpq 5084  genpcd 5109  psslinpr 5135  prlem934 5139  ltaddpr 5140  ltexprlem3 5144  ltexprlem6 5147  ltexprlem7 5148  ltapr 5151  prlem936b 5154  prlem936 5155  suplem1pr 5161  suppsr2 5223  suppsr3 5224  ltletrt 5524  xrltletrt 5563  divne0t 5729  lemul12it 5844  divgt0t 5855  divge0t 5856  nnsub 5956  lbreu 6045  sup2 6051  infmrcl 6069  bndndx 6073  xrub 6080  supxrunb2 6090  elnnz 6145  btwnnzt 6192  uzindOLD 6208  uzwo4OLD 6210  uzwo5OLD 6211  zmax 6220  zbtwnre 6221  qbtwnre 6278  ser1add2 6338  ser1add 6339  icounlem 6412  ioojoint 6416  uzwo 6455  uzwoOLD 6456  fzoptht 6502  fzrevralt 6519  le2sqit 6632  sqlecant 6641  sq01t 6651  absrpclt 6855  cau4i 6918  cau5 6919  caubnd 6926  facdivt 6942  facwordit 6944  faclbnd 6945  bccl2t 6971  clm3 7079  2climnn 7102  2climnn0 7103  climshft 7104  climaddlem3 7116  climmullem8 7127  climsqueeze 7140  climsqueeze2 7141  climsup 7155  caucvglem4 7160  caucvglem6 7162  reccnv 7218  cvgratlem1ALT 7247  cvgratlem5 7254  fsum0diag3 7260  fsum0diag4 7261  xpnnen 7499  infpnlem1 7506  infxpidmlem11 7562  uniopnt 7598  basgen2t 7639  subtop 7646  clsval2 7685  neii1 7721  neii2 7722  cncnpi 7773  cncnp 7778  metge0 7819  metxp 7834  ssbl 7855  opnin 7869  metcnp 7887  metcnpi3 7892  metcnpi4 7893  metcni 7894  metcni2 7895  lmnn 7935  metelcls 7965  metcnp4lem2 7969  metcnp4 7970  iscms2lem5 7993  lmcau 7996  cmsss 7997  bcthlem18 8016  bcthlem21 8019  bcthlem28 8026  isgrp2i 8076  grplactf1o 8098  nmoub3i 8436  blocnilem 8464  ipasslem5 8494  ubthlem5 8533  ubthlem14 8542  minvecex 8578  spwpr3OLD 8662  efifolem4 8725  efifolem5 8726  chsscm 9112  ocin 9169  ocnelt 9170  occl 9181  projlem26 9211  spansneleq 9493  spansnsst 9494  elspansn4t 9496  h1datom 9504  osumlem6 9583  spansncv 9597  nmopub2tALT 9833  nmfnleub2t 9850  nmcopexlem6 9956  nmcfnexlem6 9985  nlelch 9994  bra11 10041  hstel2t 10146  cvnbtwnt 10213  spansncv2t 10220  dmdmdt 10227  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdsl0 10237  mdexch 10262  cvexchlem 10295  atcv1t 10307  atoml 10309  atcvatlem 10312  atcvat2 10314  irred 10321  atcvat4 10324  mdsymlem3 10332  mdsymlem4 10333  sumdmdi 10342  sumdmdlem 10345  cdj1 10360  cdj3lem1 10361  ghomf1olem 10396  ee7.2a 10425  uninqs 10441  oooeqim2 10476  fiiu2 10488  fiiu2OLD 10489  truni1 10499  hmphtr 10531  qusp 10555  fillsb 10560  fipfil2 10564  fipfil2OLD 10565  oefil2 10567  neifil 10568  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588  iintlem1 10632  mrdmcd 10722  imonclem 10741  ismonc 10742  cmpmon 10743  icmpmon 10744

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

Copyright terms: Public domain