com52r - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > com52r		Structured version Visualization version GIF version

Theorem com52r 103

Description: Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.)

**Hypothesis**
Ref	Expression
com5.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))

**Assertion**
Ref	Expression
com52r	⊢ (𝜃 → (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))

**Proof of Theorem com52r**
Step	Hyp	Ref	Expression
1		com5.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
2	1	com52l 102	. 2 ⊢ (𝜒 → (𝜃 → (𝜏 → (𝜑 → (𝜓 → 𝜂)))))
3	2	com5l 100	1 ⊢ (𝜃 → (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4

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

This theorem is referenced by: (None)