Theorem wl-impchain-com-1.1 35623

Description: A degenerate form of antecedent swapping. The number '1' in the theorem name indicates that it handles a chain of length 1.

Since there is just one antecedent in the chain, there is nothing to swap. Nondegenerated forms begin with wl-impchain-com-1.2 35624, for more see there. (Contributed by Wolf Lammen, 7-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
wl-impchain-com-1.1.a	⊢ (𝜓 → 𝜑)

Assertion

Ref	Expression
wl-impchain-com-1.1	⊢ (𝜓 → 𝜑)

Proof of Theorem wl-impchain-com-1.1

Step	Hyp	Ref	Expression
1		wl-impchain-com-1.1.a	1 ⊢ (𝜓 → 𝜑)

Syntax hints:   → wi 4

This theorem is referenced by:  wl-impchain-com-1.2  35624