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

Theorem 3expa 1164
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expa  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1163 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 254 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
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 947
This theorem is referenced by:  ad4ant123  1176  ad4ant124  1177  ad4ant134  1178  ad4ant234  1179  3anidm23  1258  mp3an2  1286  mpd3an3  1299  rgen3  2494  moi2  2836  sbc3ie  2952  preq12bg  3668  issod  4209  wepo  4249  reuhypd  4360  funimass4  5438  fvtp1g  5594  f1imass  5641  fcof1o  5656  f1ofveu  5728  f1ocnvfv3  5729  acexmid  5739  2ndrn  6047  frecrdg  6271  oawordriexmid  6332  mapxpen  6708  findcard  6748  findcard2  6749  findcard2s  6750  ltapig  7110  ltanqi  7174  ltmnqi  7175  lt2addnq  7176  lt2mulnq  7177  prarloclemcalc  7274  genpassl  7296  genpassu  7297  prmuloc  7338  ltexprlemm  7372  ltexprlemfl  7381  ltexprlemfu  7383  lteupri  7389  ltaprg  7391  mul4  7858  add4  7887  cnegexlem2  7902  cnegexlem3  7903  2addsub  7940  addsubeq4  7941  muladd  8110  ltleadd  8172  reapmul1  8320  apreim  8328  receuap  8390  p1le  8564  lemul12b  8576  lbinf  8663  zdiv  9090  fzind  9117  fnn0ind  9118  uzss  9295  qmulcl  9378  qreccl  9383  xrlttr  9521  xaddass  9592  icc0r  9649  iooshf  9675  elfz5  9738  elfz0fzfz0  9843  fzind2  9956  ioo0  9977  ico0  9979  ioc0  9980  expnegap0  10241  expineg2  10242  mulexpzap  10273  expsubap  10281  expnbnd  10355  facndiv  10425  bccmpl  10440  bcval5  10449  bcpasc  10452  crim  10570  climshftlemg  11011  2sumeq2dv  11080  hash2iun  11188  dvdsval3  11393  dvdsnegb  11406  muldvds1  11414  muldvds2  11415  dvdscmul  11416  dvdsmulc  11417  dvds2ln  11422  divalgb  11518  ndvdssub  11523  gcddiv  11603  rpexp1i  11728  phiprmpw  11793  hashgcdeq  11799  innei  12227  iscnp4  12282  cnpnei  12283  cnnei  12296  cnconst  12298  ismeti  12410  isxmet2d  12412  elbl2ps  12456  elbl2  12457  xblpnfps  12462  xblpnf  12463  xblm  12481  blininf  12488  blssexps  12493  blssex  12494  blsscls2  12557  metss  12558  metrest  12570  metcn  12578  divcnap  12619  cdivcncfap  12651
  Copyright terms: Public domain W3C validator