Theorem 3imp 1145

Description: Importation inference. (Contributed by NM, 8-Apr-1994.)

Hypothesis

Ref	Expression
3imp.1	|- (ph -> (ps -> (ch -> th)))

Assertion

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

Proof of Theorem 3imp

Step	Hyp	Ref	Expression
1		df-3an 936	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2		3imp.1	. . 3 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 421	. 2 |- (((ph /\ ps) /\ ch) -> th)
4	1, 3	sylbi 187	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:  3impa  1146  3impb  1147  3impia  1148  3impib  1149  3com23  1157  3an1rs  1163  3imp1  1164  3impd  1165  syl3an2  1216  syl3an3  1217  3jao  1243  biimp3ar  1282  ltfintri  4467  ssfin  4471  nnadjoin  4521  sfintfin  4533  tfinnn  4535  nclenn  6250