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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  sbc2iedv  3124  csbie2t  3196  foco2  5959  erth  6853  distrlem1prl  7950  distrlem1pru  7951  uz11  9955  elpq  10060  divgcdcoprm0  12898  cncongr1  12900  prmpwdvds  13157  ballotfilemimin  13301  issgrpd  13780  dfgrp3mlem  13956  efltlemlt  15966  clwwlkext2edg  16829