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

Theorem 3expb 1116
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 1114 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 248 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3adant3r1  1124  3adant3r2  1125  3adant3r3  1126  3adant1l  1138  3adant1r  1139  mp3an1  1230  soinxp  4438  sotri  4748  fnfco  5093  mpt2eq3dva  5597  fovrnda  5672  ovelrn  5677  grprinvd  5724  nnmsucr  6098  ltpopr  6751  ltexprlemdisj  6762  recexprlemdisj  6786  mul4  7206  add4  7235  2addsub  7288  addsubeq4  7289  subadd4  7318  muladd  7453  ltleadd  7515  divmulap  7728  divap0  7737  div23ap  7744  div12ap  7747  divsubdirap  7759  divcanap5  7765  divmuleqap  7768  divcanap6  7770  divdiv32ap  7771  letrp1  7889  lemul12b  7902  lediv1  7910  cju  7989  nndivre  8025  nndivtr  8031  nn0addge1  8285  nn0addge2  8286  peano2uz2  8404  uzind  8408  uzind3  8410  fzind  8412  fnn0ind  8413  uzind4  8627  qre  8657  irrmul  8679  rpdivcl  8706  rerpdivcl  8711  iccshftr  8963  iccshftl  8965  iccdil  8967  icccntr  8969  fzaddel  9024  fzrev  9048  frec2uzf1od  9356  expdivap  9471  2shfti  9660  iisermulc2  10091  dvds2add  10141  dvds2sub  10142  dvdstr  10144  alzdvds  10166  divalg2  10238
  Copyright terms: Public domain W3C validator