Theorem 3exp 1103

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 1083	. 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 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3expa  1104  3expb  1105  3expia  1106  3expib  1107  3com23  1110  3an1rs  1116  3exp1  1120  3expd  1121  exp5o  1123  syl3an2  1169  syl3an3  1170  3impexpbicomi  1328  rexlimdv3a  2435  rabssdv  3020  reupick2  3223  ssorduni  4213  tfisi  4310  fvssunirng  5190  f1oiso2  5466  poxp  5853  tfrlem5  5930  nndi  6065  nnmass  6066  findcard  6345  ac6sfi  6352  mulcanpig  6433  divgt0  7838  divge0  7839  uzind  8349  uzind2  8350