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

Theorem 3exp 1202
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 1176 . 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 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  3expa  1203  3expb  1204  3expia  1205  3expib  1206  3com23  1209  3an1rs  1219  3exp1  1223  3expd  1224  exp5o  1226  syl3an2  1272  syl3an3  1273  syl2an23an  1299  3impexpbicomi  1439  rexlimdv3a  2596  rabssdv  3235  reupick2  3421  ssorduni  4485  tfisi  4585  fvssunirng  5529  f1oiso2  5825  poxp  6230  tfrlem5  6312  nndi  6484  nnmass  6485  findcard  6885  ac6sfi  6895  mulcanpig  7331  divgt0  8825  divge0  8826  uzind  9360  uzind2  9361  facavg  10719  prodfap0  11546  prodfrecap  11547  fprodabs  11617  dvdsmodexp  11795  dvdsnprmd  12117  prmndvdsfaclt  12148  fermltl  12226  pceu  12287  mulgass2  13166  fiinopn  13373  neipsm  13525  tpnei  13531  opnneiid  13535  neibl  13862  tgqioo  13918
  Copyright terms: Public domain W3C validator