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

Theorem 3expb 1105
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expb  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1103 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 244 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    /\ w3a 885
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 887
This theorem is referenced by:  3adant3r1  1113  3adant3r2  1114  3adant3r3  1115  3adant1l  1127  3adant1r  1128  mp3an1  1219  soinxp  4410  sotri  4720  fnfco  5065  mpt2eq3dva  5569  fovrnda  5644  ovelrn  5649  grprinvd  5696  nnmsucr  6067  ltpopr  6693  ltexprlemdisj  6704  recexprlemdisj  6728  mul4  7145  add4  7172  2addsub  7225  addsubeq4  7226  subadd4  7255  muladd  7381  ltleadd  7441  divmulap  7654  divap0  7663  div23ap  7670  div12ap  7673  divsubdirap  7684  divcanap5  7690  divmuleqap  7693  divcanap6  7695  divdiv32ap  7696  letrp1  7814  lemul12b  7827  lediv1  7835  cju  7913  nndivre  7949  nndivtr  7955  nn0addge1  8228  nn0addge2  8229  peano2uz2  8345  uzind  8349  uzind3  8351  fzind  8353  fnn0ind  8354  uzind4  8531  qre  8560  irrmul  8581  rpdivcl  8608  rerpdivcl  8613  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  fzaddel  8922  fzrev  8946  frec2uzf1od  9192  expdivap  9305  2shfti  9432  iisermulc2  9860
  Copyright terms: Public domain W3C validator