Theorem wl-impchain-com-1.1

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 , for more see there. (Contributed by Wolf Lammen, 7-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	wl-impchain-com-1.1.a	$$⊢\psi \to \phi$$
Assertion	wl-impchain-com-1.1	$$⊢\psi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		wl-impchain-com-1.1.a	$$⊢\psi \to \phi$$