Theorem 3exp 1204

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

Syntax hints:   -> wi 4   /\ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3expa  1205  3expb  1206  3expia  1207  3expib  1208  3com23  1211  3an1rs  1221  3exp1  1225  3expd  1226  exp5o  1228  syl3an2  1283  syl3an3  1284  syl2an23an  1310  3impexpbicomi  1450  rexlimdv3a  2613  rabssdv  3260  reupick2  3446  ssorduni  4520  tfisi  4620  fvssunirng  5570  f1oiso2  5871  poxp  6287  tfrlem5  6369  nndi  6541  nnmass  6542  findcard  6946  ac6sfi  6956  mulcanpig  7397  divgt0  8893  divge0  8894  uzind  9431  uzind2  9432  facavg  10820  prodfap0  11691  prodfrecap  11692  fprodabs  11762  dvdsmodexp  11941  dvdsaddre2b  11987  dvdsnprmd  12266  prmndvdsfaclt  12297  fermltl  12375  pceu  12436  mulgass2  13557  islss4  13881  rnglidlmcl  13979  fiinopn  14183  neipsm  14333  tpnei  14339  opnneiid  14343  neibl  14670  tgqioo  14734  gausslemma2dlem1a  15215