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  2616  rabssdv  3263  reupick2  3449  ssorduni  4523  tfisi  4623  fvssunirng  5573  f1oiso2  5874  poxp  6290  tfrlem5  6372  nndi  6544  nnmass  6545  findcard  6949  ac6sfi  6959  mulcanpig  7402  divgt0  8899  divge0  8900  uzind  9437  uzind2  9438  facavg  10838  prodfap0  11710  prodfrecap  11711  fprodabs  11781  dvdsmodexp  11960  dvdsaddre2b  12006  dvdsnprmd  12293  prmndvdsfaclt  12324  fermltl  12402  pceu  12464  mulgass2  13614  islss4  13938  rnglidlmcl  14036  fiinopn  14240  neipsm  14390  tpnei  14396  opnneiid  14400  neibl  14727  tgqioo  14791  gausslemma2dlem1a  15299