Theorem 3exp 1184

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 1161	. 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 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3expa  1185  3expb  1186  3expia  1187  3expib  1188  3com23  1191  3an1rs  1201  3exp1  1205  3expd  1206  exp5o  1208  syl3an2  1254  syl3an3  1255  syl2an23an  1281  3impexpbicomi  1419  rexlimdv3a  2576  rabssdv  3208  reupick2  3393  ssorduni  4446  tfisi  4546  fvssunirng  5483  f1oiso2  5777  poxp  6179  tfrlem5  6261  nndi  6433  nnmass  6434  findcard  6833  ac6sfi  6843  mulcanpig  7255  divgt0  8743  divge0  8744  uzind  9275  uzind2  9276  facavg  10620  prodfap0  11442  prodfrecap  11443  fprodabs  11513  dvdsmodexp  11691  dvdsnprmd  12002  prmndvdsfaclt  12031  fermltl  12109  fiinopn  12413  neipsm  12565  tpnei  12571  opnneiid  12575  neibl  12902  tgqioo  12958