Theorem 3exp 1205

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 1179	. 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 981

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 983

This theorem is referenced by:  3expa  1206  3expb  1207  3expia  1208  3expib  1209  3com23  1212  3an1rs  1222  3exp1  1226  3expd  1227  exp5o  1229  syl3an2  1284  syl3an3  1285  syl2an23an  1312  3impexpbicomi  1460  rexlimdv3a  2627  rabssdv  3281  reupick2  3467  ssorduni  4553  tfisi  4653  fvssunirng  5614  f1oiso2  5919  poxp  6341  tfrlem5  6423  nndi  6595  nnmass  6596  findcard  7011  ac6sfi  7021  mulcanpig  7483  divgt0  8980  divge0  8981  uzind  9519  uzind2  9520  facavg  10928  prodfap0  11971  prodfrecap  11972  fprodabs  12042  dvdsmodexp  12221  dvdsaddre2b  12267  dvdsnprmd  12562  prmndvdsfaclt  12593  fermltl  12671  pceu  12733  mulgass2  13935  islss4  14259  rnglidlmcl  14357  fiinopn  14591  neipsm  14741  tpnei  14747  opnneiid  14751  neibl  15078  tgqioo  15142  gausslemma2dlem1a  15650