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

Theorem anassrs 380
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 347 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 243 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  anass  381  mpanr1  413  anass1rs  505  anabss5  512  anabss7  517  2ralbida  2345  2rexbidva  2347  pofun  4049  issod  4056  imainss  4739  fvelimab  5229  eqfnfv2  5266  funconstss  5285  fnex  5383  rexima  5394  ralima  5395  f1elima  5412  fliftfun  5436  isores2  5453  isosolem  5463  f1oiso  5465  ovmpt2dxf  5626  grpridd  5697  tfrlemibxssdm  5941  oav2  6043  omv2  6045  nnaass  6064  eroveu  6197  prarloclem4  6594  genpml  6613  genpmu  6614  genpassl  6620  genpassu  6621  prmuloc2  6663  addcomprg  6674  mulcomprg  6676  ltaddpr  6693  ltexprlemloc  6703  addcanprlemu  6711  recexgt0sr  6856  reapmul1  7584  apreim  7592  recexaplem2  7631  creur  7909  uz11  8493  fzrevral  8965  iseqcaopr2  9215  expnlbnd2  9348  shftlem  9391  resqrexlemgt0  9592  cau3lem  9684  clim2  9777  clim2c  9778  clim0c  9780  2clim  9795  climabs0  9801  climcn1  9802  climcn2  9803  climsqz  9828  climsqz2  9829
  Copyright terms: Public domain W3C validator