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  560  anabss5  567  anabss7  572  2ralbida  2454  2rexbidva  2456  ralimdvva  2499  pofun  4229  issod  4236  imainss  4949  fvelimab  5470  eqfnfv2  5512  funconstss  5531  fnex  5635  rexima  5649  ralima  5650  f1elima  5667  fliftfun  5690  isores2  5707  isosolem  5718  f1oiso  5720  ovmpodxf  5889  grpridd  5960  tfrlemibxssdm  6217  oav2  6352  omv2  6354  nnaass  6374  eroveu  6513  prarloclem4  7299  genpml  7318  genpmu  7319  genpassl  7325  genpassu  7326  prmuloc2  7368  addcomprg  7379  mulcomprg  7381  ltaddpr  7398  ltexprlemloc  7408  addcanprlemu  7416  recexgt0sr  7574  reapmul1  8350  apreim  8358  recexaplem2  8406  creur  8710  uz11  9341  xaddass  9645  xleadd1a  9649  xlt2add  9656  fzrevral  9878  seq3caopr2  10248  expnlbnd2  10410  shftlem  10581  resqrexlemgt0  10785  cau3lem  10879  clim2  11045  clim2c  11046  clim0c  11048  2clim  11063  climabs0  11069  climcn1  11070  climcn2  11071  climsqz  11097  climsqz2  11098  summodclem2  11144  fsum2dlemstep  11196  fsumiun  11239  mertenslem2  11298  mertensabs  11299  prodfrecap  11308  gcdmultiplez  11698  dvdssq  11708  lcmgcdlem  11747  lcmdvds  11749  coprmdvds2  11763  neipsm  12312  lmbrf  12373  lmss  12404  txbas  12416  txbasval  12425  tx1cn  12427  txlm  12437  isxmet2d  12506  elmopn2  12607  mopni3  12642  blsscls2  12651  metequiv2  12654  metss2lem  12655  metrest  12664  metcnp  12670  metcnp2  12671  metcnpi3  12675  elcncf2  12719  mulc1cncf  12734  cncfco  12736  cncfmet  12737
  Copyright terms: Public domain W3C validator