Theorem 3exp 1150

Description: Exportation inference. (Contributed by NM, 30-May-1994.)

Hypothesis

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

Assertion

Ref	Expression
3exp	|- (ph -> (ps -> (ch -> th)))

Proof of Theorem 3exp

Step	Hyp	Ref	Expression
1		pm3.2an3 1131	. 2 |- (ph -> (ps -> (ch -> (ph /\ ps /\ ch))))
2		3exp.1	. 2 |- ((ph /\ ps /\ ch) -> th)
3	1, 2	syl8 65	1 |- (ph -> (ps -> (ch -> th)))

Syntax hints:   -> wi 4   /\ 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:  3expa  1151  3expb  1152  3expia  1153  3expib  1154  3com23  1157  3an1rs  1163  3exp1  1167  3expd  1168  exp5o  1170  syl3an2  1216  syl3an3  1217  3ecase  1286  3impexpbicomi  1368  rexlimdv3a  2741  rabssdv  3347  reupick2  3542  ssfin  4471  tfin11  4494  f1oiso2  5501  funsi  5521  trrd  5926  nchoicelem17  6306