Theorem wl-impchain-com-3.2.1 38164

Description: This theorem is in fact a copy of com3r 88. The proof is an example of how to arrive at arbitrary permutations of antecedents, using only swapping theorems. The recursion principle is to first swap the correct antecedent to the position just before the consequent, and then employ a theorem handling an implication chain of length one less to reorder the others. (Contributed by Wolf Lammen, 17-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
wl-impchain-com-3.2.1.h1	⊢ (𝜃 → (𝜒 → (𝜓 → 𝜑)))

Assertion

Ref	Expression
wl-impchain-com-3.2.1	⊢ (𝜓 → (𝜃 → (𝜒 → 𝜑)))

Proof of Theorem wl-impchain-com-3.2.1

Step	Hyp	Ref	Expression
1		wl-impchain-com-3.2.1.h1	. . 3 ⊢ (𝜃 → (𝜒 → (𝜓 → 𝜑)))
2	1	wl-impchain-com-2.3 38162	. 2 ⊢ (𝜃 → (𝜓 → (𝜒 → 𝜑)))
3	2	wl-impchain-com-1.2 38158	1 ⊢ (𝜓 → (𝜃 → (𝜒 → 𝜑)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-luk1 38124  ax-luk2 38125  ax-luk3 38126

This theorem is used by: (None)