Metamath Proof Explorer


Theorem wl-impchain-com-1.2

Description: This theorem is in fact a copy of wl-luk-com12 , and repeated here to demonstrate a simple proof scheme. The number '2' in the theorem name indicates that a chain of length 2 is modified.

See wl-impchain-com-1.x for more information how this proof is generated. (Contributed by Wolf Lammen, 7-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis wl-impchain-com.1.2.a
|- ( ch -> ( ps -> ph ) )
Assertion wl-impchain-com-1.2
|- ( ps -> ( ch -> ph ) )

Proof

Step Hyp Ref Expression
1 wl-impchain-com.1.2.a
 |-  ( ch -> ( ps -> ph ) )
2 1 wl-impchain-com-1.1
 |-  ( ch -> ( ps -> ph ) )
3 wl-luk-pm2.04
 |-  ( ( ch -> ( ps -> ph ) ) -> ( ps -> ( ch -> ph ) ) )
4 2 3 wl-impchain-mp-0
 |-  ( ps -> ( ch -> ph ) )
5 4 wl-impchain-com-1.1
 |-  ( ps -> ( ch -> ph ) )