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

Theorem 3expia 1105
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3expia

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3
213exp 1102 . 2
32imp 115 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
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 886
This theorem is referenced by:  mp3an3  1220  3gencl  2582  moi  2718  sotricim  4051  elirr  4224  en2lp  4232  suc11g  4235  3optocl  4361  sefvex  5139  f1oresrab  5272  ovmpt2s  5566  ov2gf  5567  poxp  5794  brtposg  5810  dfsmo2  5843  smoiun  5857  tfrlemibxssdm  5882  nnsucsssuc  6010  nnaordi  6017  nnawordex  6037  xpdom3m  6244  ltbtwnnqq  6398  prarloclem4  6480  addlocpr  6518  1idprl  6565  1idpru  6566  ltexprlemrnd  6578  recexprlemrnd  6600  recexprlem1ssl  6604  recexprlem1ssu  6605  recexprlemss1l  6606  recexprlemss1u  6607  aptisr  6685  axpre-apti  6749  ltxrlt  6862  axapti  6867  lttri3  6875  reapti  7343  apreap  7351  msqge0  7380  mulge0  7383  recexap  7396  mulap0b  7398  lt2msq  7613  zaddcl  8041  zdiv  8084  zextlt  8088  prime  8093  uzind2  8106  fzind  8109  lbzbi  8307  xltneg  8499  iocssre  8572  icossre  8573  iccssre  8574  fzen  8657  expival  8891  expclzaplem  8913  expnegzap  8923  expaddzap  8933  expmulzap  8935  bj-peano4  9389
  Copyright terms: Public domain W3C validator