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

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

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3 ((φ ψ χ) → θ)
213exp 1087 . 2 (φ → (ψ → (χθ)))
32imp31 243 1 (((φ ψ) χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 871
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 873
This theorem is referenced by:  3anidm23  1178  mp3an2  1203  mpd3an3  1216  rgen3  2380  moi2  2695  sbc3ie  2804  preq12bg  3514  issod  4026  reuhypd  4149  funimass4  5145  fvtp1g  5290  f1imass  5334  fcof1o  5350  f1ofveu  5420  f1ocnvfv3  5421  acexmid  5431  2ndrn  5728  rdgon  5889  frecrdg  5904  ltapig  6192  ltanqi  6255  ltmnqi  6256  lt2addnq  6257  ltbtwnnqq  6266  prarloclemcalc  6350  genpassl  6373  genpassu  6374  prmuloc  6404  ltexprlemm  6431  ltexprlemfl  6440  ltexprlemfu  6442  ltaprg  6449  mul4  6732  add4  6759  cnegexlem2  6774  cnegexlem3  6775  2addsub  6812  addsubeq4  6813  muladd  6967  ltleadd  7026
  Copyright terms: Public domain W3C validator