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  6480  addlocpr  6519  1idprl  6564  1idpru  6565  ltexprlemrnd  6577  recexprlemrnd  6599  recexprlem1ssl  6603  recexprlem1ssu  6604  recexprlemss1l  6605  recexprlemss1u  6606  aptisr  6665  axpre-apti  6729  ltxrlt  6842  axapti  6847  lttri3  6855  reapti  7323  apreap  7331  msqge0  7360  mulge0  7363  recexap  7376  mulap0b  7378  lt2msq  7593  zaddcl  8021  zdiv  8064  zextlt  8068  prime  8073  uzind2  8086  fzind  8089  lbzbi  8287  xltneg  8479  iocssre  8552  icossre  8553  iccssre  8554  fzen  8637  expival  8871  expclzaplem  8893  expnegzap  8903  expaddzap  8913  expmulzap  8915  bj-peano4  9343
  Copyright terms: Public domain W3C validator