Theorem 3exp 1138

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 1118	. 2 |- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	syl8 70	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ w3a 920

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3expa  1139  3expb  1140  3expia  1141  3expib  1142  3com23  1145  3an1rs  1151  3exp1  1155  3expd  1156  exp5o  1158  syl3an2  1204  syl3an3  1205  syl2an23an  1231  3impexpbicomi  1369  rexlimdv3a  2480  rabssdv  3075  reupick2  3257  ssorduni  4239  tfisi  4336  fvssunirng  5221  f1oiso2  5497  poxp  5884  tfrlem5  5963  nndi  6130  nnmass  6131  findcard  6422  ac6sfi  6431  mulcanpig  6587  divgt0  8017  divge0  8018  uzind  8539  uzind2  8540  facavg  9770  dvdsnprmd  10651  prmndvdsfaclt  10679