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  3124  csbie2t  3196  foco2  5949  erth  6843  distrlem1prl  7939  distrlem1pru  7940  uz11  9924  elpq  10028  divgcdcoprm0  12857  cncongr1  12859  prmpwdvds  13112  ballotfilemimin  13227  issgrpd  13704  dfgrp3mlem  13880  efltlemlt  15798  clwwlkext2edg  16577