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  2712  moi2  3018  sbc3ie  3116  preq12bg  4129  eladdci  4400  nnsucelr  4429  nndisjeq  4430  leltfintr  4459  nnpw1ex  4485  tfinpw1  4495  tfinltfinlem1  4501  tfinltfin  4502  sfin112  4530  sfindbl  4531  sfinltfin  4536  vfinncvntnn  4549  nenpw1pwlem2  6086  ncspw1eu  6160  letc  6232  ce2le  6234