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

Theorem 3exp 1184
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 1161 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 71 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 963
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 965
This theorem is referenced by:  3expa  1185  3expb  1186  3expia  1187  3expib  1188  3com23  1191  3an1rs  1201  3exp1  1205  3expd  1206  exp5o  1208  syl3an2  1254  syl3an3  1255  syl2an23an  1281  3impexpbicomi  1419  rexlimdv3a  2576  rabssdv  3208  reupick2  3393  ssorduni  4446  tfisi  4546  fvssunirng  5483  f1oiso2  5777  poxp  6179  tfrlem5  6261  nndi  6433  nnmass  6434  findcard  6833  ac6sfi  6843  mulcanpig  7255  divgt0  8743  divge0  8744  uzind  9275  uzind2  9276  facavg  10620  prodfap0  11442  prodfrecap  11443  fprodabs  11513  dvdsmodexp  11691  dvdsnprmd  12002  prmndvdsfaclt  12031  fermltl  12109  fiinopn  12413  neipsm  12565  tpnei  12571  opnneiid  12575  neibl  12902  tgqioo  12958
  Copyright terms: Public domain W3C validator