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  1459  rexlimdv3a  2625  rabssdv  3273  reupick2  3459  ssorduni  4536  tfisi  4636  fvssunirng  5593  f1oiso2  5898  poxp  6320  tfrlem5  6402  nndi  6574  nnmass  6575  findcard  6987  ac6sfi  6997  mulcanpig  7450  divgt0  8947  divge0  8948  uzind  9486  uzind2  9487  facavg  10893  prodfap0  11889  prodfrecap  11890  fprodabs  11960  dvdsmodexp  12139  dvdsaddre2b  12185  dvdsnprmd  12480  prmndvdsfaclt  12511  fermltl  12589  pceu  12651  mulgass2  13853  islss4  14177  rnglidlmcl  14275  fiinopn  14509  neipsm  14659  tpnei  14665  opnneiid  14669  neibl  14996  tgqioo  15060  gausslemma2dlem1a  15568