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

Theorem 3expb 1091
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1 ((φ ψ χ) → θ)
Assertion
Ref Expression
3expb ((φ (ψ χ)) → θ)

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1089 . 2 (φ → (ψ → (χθ)))
32imp32 244 1 ((φ (ψ χ)) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 873
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 875
This theorem is referenced by:  3adant3r1  1099  3adant3r2  1100  3adant3r3  1101  3adant1l  1113  3adant1r  1114  mp3an1  1204  soinxp  4337  sotri  4647  fnfco  4990  mpt2eq3dva  5492  fovrnda  5567  ovelrn  5572  grprinvd  5619  nnmsucr  5982  ltpopr  6432  ltexprlemdisj  6443  recexprlemdisj  6464  mul4  6732  add4  6759  2addsub  6812  addsubeq4  6813  subadd4  6841  muladd  6967
  Copyright terms: Public domain W3C validator