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  2715  rspc3v  2965  raltpg  3778  rextpg  3779  eladdci  4400  lefinlteq  4464  opelopabt  4700  3optocl  4841  fun2ssres  5146  funssfv  5344  foco2  5427  f1elima  5475  eloprabga  5579  mucass  6136  cenc  6182