Theorem impl 380

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
impl.1	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
impl	|- ( ( ( ph /\ ps ) /\ ch ) -> th )

Proof of Theorem impl

Step	Hyp	Ref	Expression
1		impl.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 258	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp31 256	1 |- ( ( ( ph /\ ps ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sbc2iedv  3118  csbie2t  3190  foco2  5932  erth  6826  distrlem1prl  7913  distrlem1pru  7914  uz11  9895  elpq  9999  divgcdcoprm0  12823  cncongr1  12825  prmpwdvds  13078  ballotfilemimin  13193  issgrpd  13675  dfgrp3mlem  13853  efltlemlt  15765  clwwlkext2edg  16543