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  3259  reupick2  3445  ssorduni  4519  tfisi  4619  fvssunirng  5569  f1oiso2  5870  poxp  6285  tfrlem5  6367  nndi  6539  nnmass  6540  findcard  6944  ac6sfi  6954  mulcanpig  7395  divgt0  8891  divge0  8892  uzind  9428  uzind2  9429  facavg  10817  prodfap0  11688  prodfrecap  11689  fprodabs  11759  dvdsmodexp  11938  dvdsaddre2b  11984  dvdsnprmd  12263  prmndvdsfaclt  12294  fermltl  12372  pceu  12433  mulgass2  13554  islss4  13878  rnglidlmcl  13976  fiinopn  14172  neipsm  14322  tpnei  14328  opnneiid  14332  neibl  14659  tgqioo  14715  gausslemma2dlem1a  15174