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 923  a4imt 1157  cbv1 1161  sbied 1194  sbequi 1227  ax11indn 1365  r19.21adva 1717  r19.21advva 1720  ralcom2 1774  reu3 1928  sbciegft 1956  reuss2 2272  reupick 2276  ssiun 2588  pwssun 2823  ralxfrd 2893  wefrc 2939  ordelord 2966  tz7.7 2969  onfr 2982  ordtr2 2998  onmindif 3056  unizlim 3109  limsssuc 3117  limomss 3133  findsg 3153  tfinds 3157  tfindsg 3158  funssres 3548  funcnvuni 3560  fv3 3728  funfvima2 3848  isoini 3895  f1oweALT 3901  tfrlem1 3906  tz7.49 3954  abianfp 3957  oarec 4189  omordi 4190  omlimcl 4202  omass 4204  oeordi 4207  oeordsuc 4214  nnmordi 4239  nnaordex 4242  nnawordex 4243  oaabs 4245  omsmolem 4249  eceqopreq 4306  th3qlem1 4307  en3d 4391  xpdom2 4431  sdomen2 4471  mapenlem2 4479  pssnn 4522  suc11reg 4588  inf3lem2 4597  inf3lem5 4600  noinfep 4623  trcl 4628  zfregs 4630  aceq5lem5 4722  zorn2lem4 4774  zorn2lem6 4776  zorn2lem7 4777  fodom 4781  uniimadom 4793  unxpdomlem 4826  alephordi 4857  ltbtwnpq 5067  genpcd 5092  psslinpr 5118  prlem934 5122  ltaddpr 5123  ltexprlem3 5127  ltexprlem6 5130  ltexprlem7 5131  ltapr 5134  prlem936b 5137  prlem936 5138  suplem1pr 5144  suppsr2 5206  suppsr3 5207  ltletrt 5507  xrltletrt 5546  divne0t 5702  lemul12it 5810  divgt0t 5819  divge0t 5820  nnsub 5913  lbreu 6002  sup2 6008  infmrcl 6026  bndndx 6030  xrub 6037  supxrunb2 6047  elnnz 6102  btwnnzt 6149  uzindOLD 6166  uzwo4OLD 6168  uzwo5OLD 6169  zmax 6178  zbtwnre 6179  qbtwnre 6228  ser1add2 6288  ser1add 6289  icounlem 6358  uzwo 6400  uzwoOLD 6401  fzoptht 6447  fzrevralt 6464  le2sqit 6577  sqlecant 6586  sq01t 6596  absrpclt 6805  cau4i 6870  cau5 6871  caubnd 6878  facdivt 6894  facwordit 6896  faclbnd 6897  bccl2t 6924  clm3 7032  2climnn 7055  2climnn0 7056  climshft 7057  climaddlem3 7069  climmullem8 7080  climsqueeze 7093  climsqueeze2 7094  climsup 7108  caucvglem4 7113  caucvglem6 7115  reccnv 7170  cvgratlem1ALT 7199  cvgratlem5 7206  fsum0diag3 7212  fsum0diag4 7213  xpnnen 7458  znnenlemOLD 7461  infpnlem1 7466  infxpidmlem11 7522  uniopnt 7558  basgen2t 7599  subtop 7606  clsval2 7645  neii1 7681  neii2 7682  cncnpi 7733  cncnp 7738  metge0 7781  metxp 7796  ssbl 7817  opnin 7831  metcnp 7849  metcnpi3 7854  metcnpi4 7855  metcni 7856  metcni2 7857  lmnn 7897  metelcls 7927  metcnp4lem2 7931  metcnp4 7932  iscms2lem5 7955  lmcau 7958  cmsss 7959  bcthlem18 7978  bcthlem21 7981  bcthlem28 7988  isgrp2i 8038  grplactf1o 8061  nmoub3i 8396  blocnilem 8423  ipasslem5 8453  ubthlem5 8492  ubthlem14 8501  minvecex 8537  efifolem4 8675  efifolem5 8676  chsscm 9067  ocin 9124  ocnelt 9125  occl 9136  projlem26 9166  spansneleq 9449  spansneleqOLD 9450  spansnsst 9451  elspansn4t 9453  h1datom 9461  osumlem6 9540  spansncv 9554  nmopub2tALT 9790  nmfnleub2t 9807  nmcopexlem6 9912  nmcfnexlem6 9941  nlelch 9950  bra11 9997  hstel2t 10102  cvnbtwnt 10169  spansncv2t 10176  dmdmdt 10183  dmdbr3 10188  dmdbr4 10189  dmdbr5 10191  mdsl0 10193  mdexch 10218  cvexchlem 10251  atcv1t 10263  atoml 10265  atcvatlem 10268  atcvat2 10270  irred 10277  atcvat4 10280  mdsymlem3 10288  mdsymlem4 10289  sumdmdi 10298  sumdmdlem 10301  cdj1 10316  cdj3lem1 10317  ghomf1olem 10352  ee7.2a 10383  uninqs 10400  oooeqim2 10429  fiiu2 10436  truni1 10445  hmphtr 10477  qusp 10489  fillsb 10494  fipfil2 10498  oefil2 10500  neifil 10501  efilcp 10504  efilcp2 10509  cnfilca 10510  rcfpfillem2 10512  iintlem1 10548  mrdmcd 10638  imonclem 10655  ismonc 10656  cmpmon 10657  icmpmon 10659

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

Copyright terms: Public domain