Theorem 3exp 1192

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 1166	. 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 968

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 970

This theorem is referenced by:  3expa  1193  3expb  1194  3expia  1195  3expib  1196  3com23  1199  3an1rs  1209  3exp1  1213  3expd  1214  exp5o  1216  syl3an2  1262  syl3an3  1263  syl2an23an  1289  3impexpbicomi  1427  rexlimdv3a  2584  rabssdv  3221  reupick2  3407  ssorduni  4463  tfisi  4563  fvssunirng  5500  f1oiso2  5794  poxp  6196  tfrlem5  6278  nndi  6450  nnmass  6451  findcard  6850  ac6sfi  6860  mulcanpig  7272  divgt0  8763  divge0  8764  uzind  9298  uzind2  9299  facavg  10655  prodfap0  11482  prodfrecap  11483  fprodabs  11553  dvdsmodexp  11731  dvdsnprmd  12053  prmndvdsfaclt  12084  fermltl  12162  pceu  12223  fiinopn  12602  neipsm  12754  tpnei  12760  opnneiid  12764  neibl  13091  tgqioo  13147