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

Theorem anassrs 398
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 363 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 254 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  anass  399  mpanr1  434  anass1rs  561  anabss5  568  anabss7  573  2ralbida  2459  2rexbidva  2461  ralimdvva  2504  pofun  4241  issod  4248  imainss  4961  fvelimab  5484  eqfnfv2  5526  funconstss  5545  fnex  5649  rexima  5663  ralima  5664  f1elima  5681  fliftfun  5704  isores2  5721  isosolem  5732  f1oiso  5734  ovmpodxf  5903  grpridd  5974  tfrlemibxssdm  6231  oav2  6366  omv2  6368  nnaass  6388  eroveu  6527  prarloclem4  7329  genpml  7348  genpmu  7349  genpassl  7355  genpassu  7356  prmuloc2  7398  addcomprg  7409  mulcomprg  7411  ltaddpr  7428  ltexprlemloc  7438  addcanprlemu  7446  recexgt0sr  7604  reapmul1  8380  apreim  8388  recexaplem2  8436  creur  8740  uz11  9371  xaddass  9681  xleadd1a  9685  xlt2add  9692  fzrevral  9915  seq3caopr2  10285  expnlbnd2  10447  shftlem  10619  resqrexlemgt0  10823  cau3lem  10917  clim2  11083  clim2c  11084  clim0c  11086  2clim  11101  climabs0  11107  climcn1  11108  climcn2  11109  climsqz  11135  climsqz2  11136  summodclem2  11182  fsum2dlemstep  11234  fsumiun  11277  mertenslem2  11336  mertensabs  11337  prodfrecap  11346  gcdmultiplez  11743  dvdssq  11753  lcmgcdlem  11792  lcmdvds  11794  coprmdvds2  11808  neipsm  12360  lmbrf  12421  lmss  12452  txbas  12464  txbasval  12473  tx1cn  12475  txlm  12485  isxmet2d  12554  elmopn2  12655  mopni3  12690  blsscls2  12699  metequiv2  12702  metss2lem  12703  metrest  12712  metcnp  12718  metcnp2  12719  metcnpi3  12723  elcncf2  12767  mulc1cncf  12782  cncfco  12784  cncfmet  12785
  Copyright terms: Public domain W3C validator