Theorem 3exp 1233

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 1207	. 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 1009

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 1011

This theorem is referenced by:  3expa  1234  3expb  1235  3expia  1236  3expib  1237  3com23  1240  3an1rs  1250  3exp1  1254  3expd  1255  exp5o  1257  syl3an2  1312  syl3an3  1313  syl2an23an  1340  3impexpbicomi  1489  rexlimdv3a  2670  rabssdv  3328  reupick2  3519  ssorduni  4629  tfisi  4729  fvssunirng  5705  f1oiso2  6023  poxp  6458  tfrlem5  6575  nndi  6749  nnmass  6750  findcard  7182  ac6sfi  7192  mulcanpig  7692  divgt0  9192  divge0  9193  uzind  9736  uzind2  9737  facavg  11162  prodfap0  12290  prodfrecap  12291  fprodabs  12361  dvdsmodexp  12540  dvdsaddre2b  12586  dvdsnprmd  12881  prmndvdsfaclt  12912  fermltl  12990  pceu  13052  mulgass2  14336  islss4  14691  rnglidlmcl  14789  fiinopn  15028  neipsm  15178  tpnei  15184  opnneiid  15188  neibl  15515  tgqioo  15579  gausslemma2dlem1a  16091  ausgrumgrien  16325  ausgrusgrien  16326  usgrausgrben  16327  ushgredgedg  16381  ushgredgedgloop  16383  wlkl1loop  16513