Theorem com3r 35

Description: Commutation of antecedents. Rotate right.

Hypothesis

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

Assertion

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

Proof of Theorem com3r

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- (ph -> (ps -> (ch -> th)))
2	1	com3l 34	. 2 |- (ps -> (ch -> (ph -> th)))
3	2	com3l 34	1 |- (ch -> (ph -> (ps -> th)))

Syntax hints:   -> wi 3

This theorem is referenced by:  moexex 1441  vtocl3ga 1857  onfr 2992  ordsssuc2 3065  limuni3 3129  fvco 3780  fvco2 3781  eqfnfv 3803  tfrlem5 3921  tz7.49 3965  omcl 4177  oecl 4178  omwordri 4209  odi 4216  omass 4217  oewordri 4225  nnmcl 4236  nnecl 4237  oaabs 4258  f1oen2g 4400  f1domg 4402  tz9.12lem3 4671  zorn2lem5 4802  zorn2lem6 4803  unidom 4818  cardlim 4862  alephordi 4885  alephval2 4913  alephval3 4914  psslinpr 5147  ltaprlem 5162  prlem936b 5166  suppsr3 5236  lbreu 6047  zneo 6202  uzwo5OLD 6213  climserzle 7147  caucvg 7163  cvgratlem2 7251  infxpidmlem12 7564  cnsscnp 7769  hausnei 7781  mettri4 7811  opnin 7866  spwmo 8652  efifolem4 8720  hlim0 9100  chintcl 9290  spansn 9475  h1datom 9499  strlem3a 10174  hstrlem3a 10182  mdexch 10257  cvbr3 10289  mdsymlem4 10328  mdsymlem6 10330  uninqs 10436  11st22nd 10448  cnvhmphb 10512  set2elt 10531  top2ind 10534  oefil2 10552  cnfilca 10562  cmpassoh 10700  cmpmon 10714

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

Copyright terms: Public domain