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  2653  rabssdv  3308  reupick2  3495  ssorduni  4591  tfisi  4691  fvssunirng  5663  f1oiso2  5978  poxp  6406  tfrlem5  6523  nndi  6697  nnmass  6698  findcard  7120  ac6sfi  7130  mulcanpig  7615  divgt0  9111  divge0  9112  uzind  9652  uzind2  9653  facavg  11071  prodfap0  12186  prodfrecap  12187  fprodabs  12257  dvdsmodexp  12436  dvdsaddre2b  12482  dvdsnprmd  12777  prmndvdsfaclt  12808  fermltl  12886  pceu  12948  mulgass2  14152  islss4  14478  rnglidlmcl  14576  fiinopn  14815  neipsm  14965  tpnei  14971  opnneiid  14975  neibl  15302  tgqioo  15366  gausslemma2dlem1a  15877  ausgrumgrien  16111  ausgrusgrien  16112  usgrausgrben  16113  ushgredgedg  16167  ushgredgedgloop  16169  wlkl1loop  16299