ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anassrs Structured version   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  2339  2rexbidva  2341  pofun  4039  issod  4046  imainss  4681  fvelimab  5170  eqfnfv2  5207  funconstss  5226  fnex  5324  rexima  5335  ralima  5336  f1elima  5353  fliftfun  5377  isores2  5394  isosolem  5404  f1oiso  5406  ovmpt2dxf  5565  grpridd  5636  tfrlemibxssdm  5879  oav2  5975  omv2  5977  nnaass  5996  eroveu  6126  prarloclem4  6473  genpml  6493  genpmu  6494  genpassl  6500  genpassu  6501  prmuloc2  6538  addcomprg  6544  mulcomprg  6546  ltaddpr  6561  ltexprlemloc  6571  addcanprlemu  6579  recexgt0sr  6653  reapmul1  7331  apreim  7339  recexaplem2  7367  creur  7643  uz11  8220  fzrevral  8683
  Copyright terms: Public domain W3C validator