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  2890  moi  3020  ltfintri  4467  tfindi  4497  nnadjoin  4521  nnpweq  4524  sfintfin  4533  tfinnn  4535  sfinltfin  4536  vfintle  4547  suc11nnc  4559  phi11lem1  4596  3optocl  4841  ndmovord  5621  ov2gf  5712  antird  5929  iserd  5943  mapvalg  6010  enprmaplem5  6081  enprmaplem6  6082  nclenc  6223  lenc  6224  nclenn  6250  nchoicelem17  6306  nchoicelem19  6308  fnfreclem3  6320