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  6569  ltexprlemdisj  6580  recexprlemdisj  6602  mul4  6942  add4  6969  2addsub  7022  addsubeq4  7023  subadd4  7051  muladd  7177  ltleadd  7236  divmulap  7436  divap0  7445  div23ap  7452  div12ap  7455  divsubdirap  7466  divcanap5  7472  divmuleqap  7475  divcanap6  7477  divdiv32ap  7478  letrp1  7595  lemul12b  7608  lediv1  7616  cju  7694  nndivre  7730  nndivtr  7736  nn0addge1  8004  nn0addge2  8005  peano2uz2  8121  uzind  8125  uzind3  8127  fzind  8129  fnn0ind  8130  uzind4  8307  qre  8336  irrmul  8356  rpdivcl  8383  rerpdivcl  8388  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  fzaddel  8692  fzrev  8716  frec2uzf1od  8873  expdivap  8959
  Copyright terms: Public domain W3C validator