Theorem wl-impchain-com-1.1 33274

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. Non-degenerated forms begin with wl-impchain-com-1.2 33275, 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	|- ( ps -> ph )

Assertion

Ref	Expression
wl-impchain-com-1.1	|- ( ps -> ph )

Proof of Theorem wl-impchain-com-1.1

Step	Hyp	Ref	Expression
1		wl-impchain-com-1.1.a	1 |- ( ps -> ph )

Syntax hints:   -> wi 4

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