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 ) ) )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used 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  4636  tfisi  4736  fvssunirng  5713  f1oiso2  6036  poxp  6472  tfrlem5  6589  nndi  6763  nnmass  6764  findcard  7196  ac6sfi  7206  mulcanpig  7708  divgt0  9210  divge0  9211  uzind  9768  uzind2  9769  facavg  11206  prodfap0  12337  prodfrecap  12338  fprodabs  12408  dvdsmodexp  12587  dvdsaddre2b  12633  dvdsnprmd  12928  prmndvdsfaclt  12960  fermltl  13041  pceu  13103  mulgass2  14470  islss4  14828  rnglidlmcl  14926  fiinopn  15230  neipsm  15380  tpnei  15386  opnneiid  15390  neibl  15717  tgqioo  15781  bcmono  16304  gausslemma2dlem1a  16382  ausgrumgrien  16616  ausgrusgrien  16617  usgrausgrben  16618  ushgredgedg  16672  ushgredgedgloop  16674  wlkl1loop  16804