Theorem 3exp 1142

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 1122	. 2 |- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
2		3exp.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
3	1, 2	syl8 70	1 |- ( ph -> ( ps -> ( ch -> th ) ) )

Syntax hints:   -> wi 4   /\ w3a 924

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

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  3expa  1143  3expb  1144  3expia  1145  3expib  1146  3com23  1149  3an1rs  1155  3exp1  1159  3expd  1160  exp5o  1162  syl3an2  1208  syl3an3  1209  syl2an23an  1235  3impexpbicomi  1373  rexlimdv3a  2491  rabssdv  3101  reupick2  3285  ssorduni  4304  tfisi  4402  fvssunirng  5320  f1oiso2  5606  poxp  5997  tfrlem5  6079  nndi  6247  nnmass  6248  findcard  6604  ac6sfi  6614  mulcanpig  6894  divgt0  8333  divge0  8334  uzind  8857  uzind2  8858  facavg  10154  dvdsnprmd  11385  prmndvdsfaclt  11413  fiinopn  11601