Theorem 3impia 1148

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 |- ((ph /\ ps) -> (ch -> th))
2	1	ex 423	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 1145	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934

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  df-3an 936

This theorem is referenced by:  mopick2  2271  3gencl  2890  mob2  3017  moi  3020  reupick3  3541  disjne  3597  tfindi  4497  sfin112  4530  sfinltfin  4536  vfintle  4547  fvun1  5380  ovmpt4g  5711  ov2gf  5712  letc  6232  nclenn  6250  nchoicelem9  6298  nchoicelem17  6306  frecxp  6315