Theorem 3exp 1202

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 1176	. 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 978

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 980

This theorem is referenced by:  3expa  1203  3expb  1204  3expia  1205  3expib  1206  3com23  1209  3an1rs  1219  3exp1  1223  3expd  1224  exp5o  1226  syl3an2  1272  syl3an3  1273  syl2an23an  1299  3impexpbicomi  1439  rexlimdv3a  2596  rabssdv  3236  reupick2  3422  ssorduni  4487  tfisi  4587  fvssunirng  5531  f1oiso2  5828  poxp  6233  tfrlem5  6315  nndi  6487  nnmass  6488  findcard  6888  ac6sfi  6898  mulcanpig  7334  divgt0  8829  divge0  8830  uzind  9364  uzind2  9365  facavg  10726  prodfap0  11553  prodfrecap  11554  fprodabs  11624  dvdsmodexp  11802  dvdsaddre2b  11848  dvdsnprmd  12125  prmndvdsfaclt  12156  fermltl  12234  pceu  12295  mulgass2  13235  fiinopn  13507  neipsm  13657  tpnei  13663  opnneiid  13667  neibl  13994  tgqioo  14050