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

Theorem anassrs 386
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 351 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 247 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  anass  387  mpanr1  421  anass1rs  513  anabss5  520  anabss7  525  2ralbida  2362  2rexbidva  2364  pofun  4077  issod  4084  imainss  4767  fvelimab  5257  eqfnfv2  5294  funconstss  5313  fnex  5411  rexima  5422  ralima  5423  f1elima  5440  fliftfun  5464  isores2  5481  isosolem  5491  f1oiso  5493  ovmpt2dxf  5654  grpridd  5725  tfrlemibxssdm  5972  oav2  6074  omv2  6076  nnaass  6095  eroveu  6228  prarloclem4  6654  genpml  6673  genpmu  6674  genpassl  6680  genpassu  6681  prmuloc2  6723  addcomprg  6734  mulcomprg  6736  ltaddpr  6753  ltexprlemloc  6763  addcanprlemu  6771  recexgt0sr  6916  reapmul1  7660  apreim  7668  recexaplem2  7707  creur  7987  uz11  8591  fzrevral  9069  iseqcaopr2  9405  expnlbnd2  9542  shftlem  9645  resqrexlemgt0  9847  cau3lem  9941  clim2  10035  clim2c  10036  clim0c  10038  2clim  10053  climabs0  10059  climcn1  10060  climcn2  10061  climsqz  10086  climsqz2  10087
  Copyright terms: Public domain W3C validator