Theorem 3exp 1226

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 1200	. 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 1002

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 1004

This theorem is referenced by:  3expa  1227  3expb  1228  3expia  1229  3expib  1230  3com23  1233  3an1rs  1243  3exp1  1247  3expd  1248  exp5o  1250  syl3an2  1305  syl3an3  1306  syl2an23an  1333  3impexpbicomi  1482  rexlimdv3a  2650  rabssdv  3304  reupick2  3490  ssorduni  4579  tfisi  4679  fvssunirng  5642  f1oiso2  5951  poxp  6378  tfrlem5  6460  nndi  6632  nnmass  6633  findcard  7050  ac6sfi  7060  mulcanpig  7522  divgt0  9019  divge0  9020  uzind  9558  uzind2  9559  facavg  10968  prodfap0  12056  prodfrecap  12057  fprodabs  12127  dvdsmodexp  12306  dvdsaddre2b  12352  dvdsnprmd  12647  prmndvdsfaclt  12678  fermltl  12756  pceu  12818  mulgass2  14021  islss4  14346  rnglidlmcl  14444  fiinopn  14678  neipsm  14828  tpnei  14834  opnneiid  14838  neibl  15165  tgqioo  15229  gausslemma2dlem1a  15737  ausgrumgrien  15968  ausgrusgrien  15969  usgrausgrben  15970  ushgredgedg  16024  ushgredgedgloop  16026  wlkl1loop  16069