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  4040  issod  4047  imainss  4682  fvelimab  5172  eqfnfv2  5209  funconstss  5228  fnex  5326  rexima  5337  ralima  5338  f1elima  5355  fliftfun  5379  isores2  5396  isosolem  5406  f1oiso  5408  ovmpt2dxf  5568  grpridd  5639  tfrlemibxssdm  5882  oav2  5982  omv2  5984  nnaass  6003  eroveu  6133  prarloclem4  6481  genpml  6500  genpmu  6501  genpassl  6507  genpassu  6508  prmuloc2  6548  addcomprg  6554  mulcomprg  6556  ltaddpr  6571  ltexprlemloc  6581  addcanprlemu  6589  recexgt0sr  6701  reapmul1  7379  apreim  7387  recexaplem2  7415  creur  7692  uz11  8271  fzrevral  8737  expnlbnd2  9027
  Copyright terms: Public domain W3C validator