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  2739  ncfinraise  4481  ncfinlower  4483  tfin11  4493  tfinpw1  4494  tfinltfinlem1  4500  tfinltfin  4501  evenodddisj  4516  nnpweq  4523  sfin112  4529  sfindbl  4530  tfinnn  4534  vfinspss  4551  funiunfv  5467  erth  5968  enprmaplem3  6078  peano4nc  6150  ncssfin  6151  nntccl  6170  leltctr  6212  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem17  6305  fnfrec  6320