Theorem 3exp 1197

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 1171	. 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 973

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 975

This theorem is referenced by:  3expa  1198  3expb  1199  3expia  1200  3expib  1201  3com23  1204  3an1rs  1214  3exp1  1218  3expd  1219  exp5o  1221  syl3an2  1267  syl3an3  1268  syl2an23an  1294  3impexpbicomi  1432  rexlimdv3a  2589  rabssdv  3227  reupick2  3413  ssorduni  4471  tfisi  4571  fvssunirng  5511  f1oiso2  5806  poxp  6211  tfrlem5  6293  nndi  6465  nnmass  6466  findcard  6866  ac6sfi  6876  mulcanpig  7297  divgt0  8788  divge0  8789  uzind  9323  uzind2  9324  facavg  10680  prodfap0  11508  prodfrecap  11509  fprodabs  11579  dvdsmodexp  11757  dvdsnprmd  12079  prmndvdsfaclt  12110  fermltl  12188  pceu  12249  fiinopn  12796  neipsm  12948  tpnei  12954  opnneiid  12958  neibl  13285  tgqioo  13341