Theorem 3impa 1146

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

Hypothesis

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

Assertion

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

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 587	. 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-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:  3impdir  1238  syl3an9b  1250  biimp3a  1281  rspec3  2714  rspc3v  2964  raltpg  3777  rextpg  3778  eladdci  4399  lefinlteq  4463  opelopabt  4699  3optocl  4840  fun2ssres  5145  funssfv  5343  foco2  5426  f1elima  5474  eloprabga  5578  mucass  6135  cenc  6181