Theorem com15 11321

Description: Commutation of antecedents. Swap 1st and 5th.

Hypothesis

Ref	Expression
com5.1	⊢ (φ → (ψ → (χ → (θ → (τ → η)))))

Assertion

Ref	Expression
com15	⊢ (τ → (ψ → (χ → (θ → (φ → η)))))

Proof of Theorem com15

Step	Hyp	Ref	Expression
1		com5.1	. . . 4 ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))
2	1	com14 38	. . 3 ⊢ (θ → (ψ → (χ → (φ → (τ → η)))))
3	2	com45 11318	. 2 ⊢ (θ → (ψ → (χ → (τ → (φ → η)))))
4	3	com14 38	1 ⊢ (τ → (ψ → (χ → (θ → (φ → η)))))

Syntax hints:   → wi 3

This theorem is referenced by:  com5l 11322  cncomp 11487  fnejoin2 11585  filssufillem 11648

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

Copyright terms: Public domain