Theorem expr 598

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

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

Assertion

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

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 588	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp 418	1 |- ((ph /\ ps) -> (ch -> th))

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  rexlimdvaa  2740  ncfinraise  4482  ncfinlower  4484  tfin11  4494  tfinpw1  4495  tfinltfinlem1  4501  tfinltfin  4502  evenodddisj  4517  nnpweq  4524  sfin112  4530  sfindbl  4531  tfinnn  4535  vfinspss  4552  funiunfv  5468  erth  5969  enprmaplem3  6079  peano4nc  6151  ncssfin  6152  nntccl  6171  leltctr  6213  tlecg  6231  nchoicelem6  6295  nchoicelem8  6297  nchoicelem17  6306  fnfrec  6321