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

Theorem anassrs 395
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anassrs.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
anassrs (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem anassrs
StepHypRef Expression
1 anassrs.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 360 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 254 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  anass  396  mpanr1  431  anass1rs  543  anabss5  550  anabss7  555  2ralbida  2428  2rexbidva  2430  ralimdvva  2473  pofun  4192  issod  4199  imainss  4910  fvelimab  5429  eqfnfv2  5471  funconstss  5490  fnex  5594  rexima  5608  ralima  5609  f1elima  5626  fliftfun  5649  isores2  5666  isosolem  5677  f1oiso  5679  ovmpodxf  5848  grpridd  5919  tfrlemibxssdm  6176  oav2  6311  omv2  6313  nnaass  6333  eroveu  6472  prarloclem4  7248  genpml  7267  genpmu  7268  genpassl  7274  genpassu  7275  prmuloc2  7317  addcomprg  7328  mulcomprg  7330  ltaddpr  7347  ltexprlemloc  7357  addcanprlemu  7365  recexgt0sr  7510  reapmul1  8269  apreim  8277  recexaplem2  8320  creur  8621  uz11  9244  xaddass  9539  xleadd1a  9543  xlt2add  9550  fzrevral  9772  seq3caopr2  10142  expnlbnd2  10304  shftlem  10475  resqrexlemgt0  10678  cau3lem  10772  clim2  10938  clim2c  10939  clim0c  10941  2clim  10956  climabs0  10962  climcn1  10963  climcn2  10964  climsqz  10990  climsqz2  10991  summodclem2  11037  fsum2dlemstep  11089  fsumiun  11132  mertenslem2  11191  mertensabs  11192  gcdmultiplez  11549  dvdssq  11559  lcmgcdlem  11598  lcmdvds  11600  coprmdvds2  11614  neipsm  12160  lmbrf  12220  lmss  12251  txbas  12263  txbasval  12272  tx1cn  12274  txlm  12284  isxmet2d  12331  elmopn2  12432  mopni3  12467  blsscls2  12476  metequiv2  12479  metss2lem  12480  metrest  12489  metcnp  12495  metcnp2  12496  metcnpi3  12500  elcncf2  12541  mulc1cncf  12556  cncfco  12558  cncfmet  12559
  Copyright terms: Public domain W3C validator