Metamath Proof Explorer


Theorem animpimp2impd

Description: Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022)

Ref Expression
Hypotheses animpimp2impd.1
|- ( ( ps /\ ph ) -> ( ch -> ( th -> et ) ) )
animpimp2impd.2
|- ( ( ps /\ ( ph /\ th ) ) -> ( et -> ta ) )
Assertion animpimp2impd
|- ( ph -> ( ( ps -> ch ) -> ( ps -> ( th -> ta ) ) ) )

Proof

Step Hyp Ref Expression
1 animpimp2impd.1
 |-  ( ( ps /\ ph ) -> ( ch -> ( th -> et ) ) )
2 animpimp2impd.2
 |-  ( ( ps /\ ( ph /\ th ) ) -> ( et -> ta ) )
3 2 expr
 |-  ( ( ps /\ ph ) -> ( th -> ( et -> ta ) ) )
4 3 a2d
 |-  ( ( ps /\ ph ) -> ( ( th -> et ) -> ( th -> ta ) ) )
5 1 4 syld
 |-  ( ( ps /\ ph ) -> ( ch -> ( th -> ta ) ) )
6 5 expcom
 |-  ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
7 6 a2d
 |-  ( ph -> ( ( ps -> ch ) -> ( ps -> ( th -> ta ) ) ) )