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

Theorem anassrs 397
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 362 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 254 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
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 is referenced by:  anass  398  mpanr1  433  anass1rs  545  anabss5  552  anabss7  557  2ralbida  2433  2rexbidva  2435  ralimdvva  2478  pofun  4204  issod  4211  imainss  4924  fvelimab  5445  eqfnfv2  5487  funconstss  5506  fnex  5610  rexima  5624  ralima  5625  f1elima  5642  fliftfun  5665  isores2  5682  isosolem  5693  f1oiso  5695  ovmpodxf  5864  grpridd  5935  tfrlemibxssdm  6192  oav2  6327  omv2  6329  nnaass  6349  eroveu  6488  prarloclem4  7274  genpml  7293  genpmu  7294  genpassl  7300  genpassu  7301  prmuloc2  7343  addcomprg  7354  mulcomprg  7356  ltaddpr  7373  ltexprlemloc  7383  addcanprlemu  7391  recexgt0sr  7549  reapmul1  8324  apreim  8332  recexaplem2  8380  creur  8681  uz11  9304  xaddass  9607  xleadd1a  9611  xlt2add  9618  fzrevral  9840  seq3caopr2  10210  expnlbnd2  10372  shftlem  10543  resqrexlemgt0  10747  cau3lem  10841  clim2  11007  clim2c  11008  clim0c  11010  2clim  11025  climabs0  11031  climcn1  11032  climcn2  11033  climsqz  11059  climsqz2  11060  summodclem2  11106  fsum2dlemstep  11158  fsumiun  11201  mertenslem2  11260  mertensabs  11261  gcdmultiplez  11621  dvdssq  11631  lcmgcdlem  11670  lcmdvds  11672  coprmdvds2  11686  neipsm  12234  lmbrf  12295  lmss  12326  txbas  12338  txbasval  12347  tx1cn  12349  txlm  12359  isxmet2d  12428  elmopn2  12529  mopni3  12564  blsscls2  12573  metequiv2  12576  metss2lem  12577  metrest  12586  metcnp  12592  metcnp2  12593  metcnpi3  12597  elcncf2  12641  mulc1cncf  12656  cncfco  12658  cncfmet  12659
  Copyright terms: Public domain W3C validator