Theorem 3exp 1228

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 1202	. 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 1004

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 1006

This theorem is referenced by:  3expa  1229  3expb  1230  3expia  1231  3expib  1232  3com23  1235  3an1rs  1245  3exp1  1249  3expd  1250  exp5o  1252  syl3an2  1307  syl3an3  1308  syl2an23an  1335  3impexpbicomi  1484  rexlimdv3a  2652  rabssdv  3307  reupick2  3493  ssorduni  4585  tfisi  4685  fvssunirng  5654  f1oiso2  5968  poxp  6397  tfrlem5  6480  nndi  6654  nnmass  6655  findcard  7077  ac6sfi  7087  mulcanpig  7555  divgt0  9052  divge0  9053  uzind  9591  uzind2  9592  facavg  11009  prodfap0  12108  prodfrecap  12109  fprodabs  12179  dvdsmodexp  12358  dvdsaddre2b  12404  dvdsnprmd  12699  prmndvdsfaclt  12730  fermltl  12808  pceu  12870  mulgass2  14074  islss4  14399  rnglidlmcl  14497  fiinopn  14731  neipsm  14881  tpnei  14887  opnneiid  14891  neibl  15218  tgqioo  15282  gausslemma2dlem1a  15790  ausgrumgrien  16024  ausgrusgrien  16025  usgrausgrben  16026  ushgredgedg  16080  ushgredgedgloop  16082  wlkl1loop  16212