Theorem 3expia 1153

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 1150	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp 418	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:  mp3an3  1266  3gencl  2889  moi  3019  ltfintri  4466  tfindi  4496  nnadjoin  4520  nnpweq  4523  sfintfin  4532  tfinnn  4534  sfinltfin  4535  vfintle  4546  suc11nnc  4558  phi11lem1  4595  3optocl  4840  ndmovord  5620  ov2gf  5711  antird  5928  iserd  5942  mapvalg  6009  enprmaplem5  6080  enprmaplem6  6081  nclenc  6222  lenc  6223  nclenn  6249  nchoicelem17  6305  nchoicelem19  6307  fnfreclem3  6319