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 2

This theorem is referenced by:  moexex 1058  vtocl3ga 1389  onfr 2237  limsuclem 2360  fvco 2865  fvco2 2866  cleqfv 2880  tfrlem5 2953  tz7.49 2997  omcl 3139  oecl 3140  nnmcl 3173  nndi 3180  nnmass 3181  f1oeng 3298  f1domg 3299  tz9.12lem3 3505  zornlem5 3607  zornlem6 3608  cardlim 3657  alephordi 3679  psslinpr 3929  ltaprlem 3944  prlem936b 3948  suppsr3 4018  zneo 4601  zmax 4618  zbtwnre 4619  clim0 4882  infxpidmlem12 4944  hlim0 5140  shscl 5282  chintcl 5296  spansn 5462  h1datom 5483  strlem3a 5693  mdsymlem4 5779  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org