Theorem 3exp 1229

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 1203	. 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 1005

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 1007

This theorem is referenced by:  3expa  1230  3expb  1231  3expia  1232  3expib  1233  3com23  1236  3an1rs  1246  3exp1  1250  3expd  1251  exp5o  1253  syl3an2  1308  syl3an3  1309  syl2an23an  1336  3impexpbicomi  1485  rexlimdv3a  2664  rabssdv  3322  reupick2  3511  ssorduni  4614  tfisi  4714  fvssunirng  5690  f1oiso2  6006  poxp  6441  tfrlem5  6558  nndi  6732  nnmass  6733  findcard  7158  ac6sfi  7168  mulcanpig  7666  divgt0  9163  divge0  9164  uzind  9707  uzind2  9708  facavg  11133  prodfap0  12256  prodfrecap  12257  fprodabs  12327  dvdsmodexp  12506  dvdsaddre2b  12552  dvdsnprmd  12847  prmndvdsfaclt  12878  fermltl  12956  pceu  13018  mulgass2  14301  islss4  14656  rnglidlmcl  14754  fiinopn  14995  neipsm  15145  tpnei  15151  opnneiid  15155  neibl  15482  tgqioo  15546  gausslemma2dlem1a  16057  ausgrumgrien  16291  ausgrusgrien  16292  usgrausgrben  16293  ushgredgedg  16347  ushgredgedgloop  16349  wlkl1loop  16479