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

Theorem 3exp 1103
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 1083 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( ph  /\  ps  /\  ch ) ) ) )
2 3exp.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
31, 2syl8 65 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  3expa  1104  3expb  1105  3expia  1106  3expib  1107  3com23  1110  3an1rs  1116  3exp1  1120  3expd  1121  exp5o  1123  syl3an2  1169  syl3an3  1170  3impexpbicomi  1328  rexlimdv3a  2435  rabssdv  3020  reupick2  3223  ssorduni  4213  tfisi  4310  fvssunirng  5190  f1oiso2  5466  poxp  5853  tfrlem5  5930  nndi  6065  nnmass  6066  findcard  6345  ac6sfi  6352  mulcanpig  6433  divgt0  7838  divge0  7839  uzind  8349  uzind2  8350
  Copyright terms: Public domain W3C validator