Theorem 3exp 1137

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 1117	. 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 919

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 921

This theorem is referenced by:  3expa  1138  3expb  1139  3expia  1140  3expib  1141  3com23  1144  3an1rs  1150  3exp1  1154  3expd  1155  exp5o  1157  syl3an2  1203  syl3an3  1204  syl2an23an  1230  3impexpbicomi  1368  rexlimdv3a  2479  rabssdv  3074  reupick2  3250  ssorduni  4231  tfisi  4328  fvssunirng  5210  f1oiso2  5486  poxp  5873  tfrlem5  5953  nndi  6088  nnmass  6089  findcard  6372  ac6sfi  6379  mulcanpig  6525  divgt0  7950  divge0  7951  uzind  8458  uzind2  8459  facavg  9673  dvdsnprmd  10507  prmndvdsfaclt  10535