ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3exp Unicode version

Theorem 3exp 1138
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
StepHypRef Expression
1 pm3.2an3 1118 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 70 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
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 922
This theorem is referenced by:  3expa  1139  3expb  1140  3expia  1141  3expib  1142  3com23  1145  3an1rs  1151  3exp1  1155  3expd  1156  exp5o  1158  syl3an2  1204  syl3an3  1205  syl2an23an  1231  3impexpbicomi  1369  rexlimdv3a  2480  rabssdv  3075  reupick2  3257  ssorduni  4239  tfisi  4336  fvssunirng  5221  f1oiso2  5497  poxp  5884  tfrlem5  5963  nndi  6130  nnmass  6131  findcard  6422  ac6sfi  6431  mulcanpig  6587  divgt0  8017  divge0  8018  uzind  8539  uzind2  8540  facavg  9770  dvdsnprmd  10651  prmndvdsfaclt  10679
  Copyright terms: Public domain W3C validator