Theorem 3expa 1151

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 1150	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 421	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:  3anidm23  1241  mp3an2  1265  mpd3an3  1278  rgen3  2711  moi2  3017  sbc3ie  3115  preq12bg  4128  eladdci  4399  nnsucelr  4428  nndisjeq  4429  leltfintr  4458  nnpw1ex  4484  tfinpw1  4494  tfinltfinlem1  4500  tfinltfin  4501  sfin112  4529  sfindbl  4530  sfinltfin  4535  vfinncvntnn  4548  nenpw1pwlem2  6085  ncspw1eu  6159  letc  6231  ce2le  6233