ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3expia Structured version   GIF 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  6481  addlocpr  6519  1idprl  6566  1idpru  6567  ltexprlemrnd  6579  recexprlemrnd  6601  recexprlem1ssl  6605  recexprlem1ssu  6606  recexprlemss1l  6607  recexprlemss1u  6608  aptisr  6705  axpre-apti  6769  ltxrlt  6882  axapti  6887  lttri3  6895  reapti  7363  apreap  7371  msqge0  7400  mulge0  7403  recexap  7416  mulap0b  7418  lt2msq  7633  zaddcl  8061  zdiv  8104  zextlt  8108  prime  8113  uzind2  8126  fzind  8129  lbzbi  8327  xltneg  8519  iocssre  8592  icossre  8593  iccssre  8594  fzen  8677  expival  8911  expclzaplem  8933  expnegzap  8943  expaddzap  8953  expmulzap  8955  bj-peano4  9415
  Copyright terms: Public domain W3C validator