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

Theorem 3impb 1160
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 360 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1158 1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3adant1l  1191  3adant1r  1192  3impdi  1254  vtocl3gf  2721  rspc2ev  2776  reuss  3325  trssord  4270  funtp  5144  resdif  5355  funimass4  5438  fnovex  5770  fnotovb  5780  fovrn  5879  fnovrn  5884  fmpoco  6079  nndi  6348  nnaordi  6370  ecovass  6504  ecoviass  6505  ecovdi  6506  ecovidi  6507  eqsupti  6849  addasspig  7102  mulasspig  7104  distrpig  7105  distrnq0  7231  addassnq0  7234  distnq0r  7235  prcdnql  7256  prcunqu  7257  genpassl  7296  genpassu  7297  genpassg  7298  distrlem1prl  7354  distrlem1pru  7355  ltexprlemopl  7373  ltexprlemopu  7375  le2tri3i  7836  cnegexlem1  7901  subadd  7929  addsub  7937  subdi  8111  submul2  8125  div12ap  8417  diveqap1  8428  divnegap  8429  divdivap2  8447  ltmulgt11  8582  gt0div  8588  ge0div  8589  uzind3  9118  fnn0ind  9121  qdivcl  9387  irrmul  9391  xrlttr  9532  fzen  9774  lenegsq  10818  moddvds  11409  dvds2add  11434  dvds2sub  11435  dvdsleabs  11450  divalgb  11529  ndvdsadd  11535  modgcd  11586  absmulgcd  11612  setsresg  11903  unopn  12078  innei  12238  cncfi  12640
  Copyright terms: Public domain W3C validator