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

Theorem anassrs 392
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
anassrs  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
21exp32 357 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 252 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
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 is referenced by:  anass  393  mpanr1  428  anass1rs  536  anabss5  543  anabss7  548  2ralbida  2388  2rexbidva  2390  pofun  4075  issod  4082  imainss  4769  fvelimab  5261  eqfnfv2  5298  funconstss  5317  fnex  5415  rexima  5426  ralima  5427  f1elima  5444  fliftfun  5467  isores2  5484  isosolem  5494  f1oiso  5496  ovmpt2dxf  5657  grpridd  5728  tfrlemibxssdm  5976  oav2  6107  omv2  6109  nnaass  6129  eroveu  6263  prarloclem4  6750  genpml  6769  genpmu  6770  genpassl  6776  genpassu  6777  prmuloc2  6819  addcomprg  6830  mulcomprg  6832  ltaddpr  6849  ltexprlemloc  6859  addcanprlemu  6867  recexgt0sr  7012  reapmul1  7762  apreim  7770  recexaplem2  7809  creur  8103  uz11  8722  fzrevral  9198  iseqcaopr2  9557  expnlbnd2  9695  shftlem  9842  resqrexlemgt0  10044  cau3lem  10138  clim2  10260  clim2c  10261  clim0c  10263  2clim  10278  climabs0  10284  climcn1  10285  climcn2  10286  climsqz  10311  climsqz2  10312  gcdmultiplez  10554  dvdssq  10564  lcmgcdlem  10603  lcmdvds  10605  coprmdvds2  10619
  Copyright terms: Public domain W3C validator