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-1 5  ax-2 6  ax-3 7  ax-mp 8

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

This theorem is referenced by:  mopick2  2271  3gencl  2889  mob2  3016  moi  3019  reupick3  3540  disjne  3596  tfindi  4496  sfin112  4529  sfinltfin  4535  vfintle  4546  fvun1  5379  ovmpt4g  5710  ov2gf  5711  letc  6231  nclenn  6249  nchoicelem9  6297  nchoicelem17  6305  frecxp  6314