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

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
StepHypRef Expression
1 pm3.2an3 1122 . 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 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
  Copyright terms: Public domain W3C validator