Metamath Proof Explorer


Theorem wl-impchain-com-1.3

Description: This theorem is in fact a copy of com13 , and repeated here to demonstrate a simple proof scheme. The number '3' in the theorem name indicates that a chain of length 3 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.3.h1
|- ( th -> ( ch -> ( ps -> ph ) ) )
Assertion wl-impchain-com-1.3
|- ( ps -> ( ch -> ( th -> ph ) ) )

Proof

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