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

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

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 357 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1137 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  3adant1l  1166  3adant1r  1167  3impdi  1229  vtocl3gf  2682  rspc2ev  2735  reuss  3278  trssord  4198  funtp  5053  resdif  5259  funimass4  5339  fnovex  5664  fnotovb  5674  fovrn  5769  fnovrn  5774  fmpt2co  5963  nndi  6229  nnaordi  6247  ecovass  6381  ecoviass  6382  ecovdi  6383  ecovidi  6384  eqsupti  6670  addasspig  6868  mulasspig  6870  distrpig  6871  distrnq0  6997  addassnq0  7000  distnq0r  7001  prcdnql  7022  prcunqu  7023  genpassl  7062  genpassu  7063  genpassg  7064  distrlem1prl  7120  distrlem1pru  7121  ltexprlemopl  7139  ltexprlemopu  7141  le2tri3i  7572  cnegexlem1  7636  subadd  7664  addsub  7672  subdi  7842  submul2  7856  div12ap  8135  diveqap1  8146  divnegap  8147  divdivap2  8165  ltmulgt11  8297  gt0div  8303  ge0div  8304  uzind3  8829  fnn0ind  8832  qdivcl  9097  irrmul  9101  xrlttr  9234  fzen  9426  iseqval  9835  lenegsq  10492  moddvds  10885  dvds2add  10910  dvds2sub  10911  dvdsleabs  10926  divalgb  11005  ndvdsadd  11011  modgcd  11062  absmulgcd  11086
  Copyright terms: Public domain W3C validator