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  4535  tfisi  4635  fvssunirng  5591  f1oiso2  5896  poxp  6318  tfrlem5  6400  nndi  6572  nnmass  6573  findcard  6985  ac6sfi  6995  mulcanpig  7448  divgt0  8945  divge0  8946  uzind  9484  uzind2  9485  facavg  10891  prodfap0  11856  prodfrecap  11857  fprodabs  11927  dvdsmodexp  12106  dvdsaddre2b  12152  dvdsnprmd  12447  prmndvdsfaclt  12478  fermltl  12556  pceu  12618  mulgass2  13820  islss4  14144  rnglidlmcl  14242  fiinopn  14476  neipsm  14626  tpnei  14632  opnneiid  14636  neibl  14963  tgqioo  15027  gausslemma2dlem1a  15535