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

Theorem 3expb 1104
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 1102 . 2 (φ → (ψ → (χθ)))
32imp32 244 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:  3adant3r1  1112  3adant3r2  1113  3adant3r3  1114  3adant1l  1126  3adant1r  1127  mp3an1  1218  soinxp  4353  sotri  4663  fnfco  5008  mpt2eq3dva  5511  fovrnda  5586  ovelrn  5591  grprinvd  5638  nnmsucr  6006  ltpopr  6567  ltexprlemdisj  6578  recexprlemdisj  6600  mul4  6902  add4  6929  2addsub  6982  addsubeq4  6983  subadd4  7011  muladd  7137  ltleadd  7196  divmulap  7396  divap0  7405  div23ap  7412  div12ap  7415  divsubdirap  7426  divcanap5  7432  divmuleqap  7435  divcanap6  7437  divdiv32ap  7438  letrp1  7555  lemul12b  7568  lediv1  7576  cju  7654  nndivre  7690  nndivtr  7696  nn0addge1  7964  nn0addge2  7965  peano2uz2  8081  uzind  8085  uzind3  8087  fzind  8089  fnn0ind  8090  uzind4  8267  qre  8296  irrmul  8316  rpdivcl  8343  rerpdivcl  8348  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  fzaddel  8652  fzrev  8676  frec2uzf1od  8833  expdivap  8919
  Copyright terms: Public domain W3C validator