MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anassrs Structured version   Visualization version   GIF version

Theorem 3anassrs 1360
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypothesis
Ref Expression
3anassrs.1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
3anassrs ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem 3anassrs
StepHypRef Expression
1 3anassrs.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
213exp2 1354 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 425 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088
This theorem is referenced by:  ralrimivvva  3204  euotd  5517  dfgrp3e  19059  kerf1ghm  19266  psgndif  21621  neiptopnei  23141  neitr  23189  neitx  23616  cnextcn  24076  utoptop  24244  ustuqtoplem  24249  ustuqtop1  24251  utopsnneiplem  24257  utop3cls  24261  neipcfilu  24306  xmetpsmet  24359  metustsym  24569  grporcan  30538  disjdsct  32713  xrofsup  32772  omndmul2  33090  archirngz  33197  archiabllem1  33201  archiabllem2c  33203  reofld  33373  prmidl2  33470  pstmfval  33896  tpr2rico  33912  esumpcvgval  34080  esumcvg  34088  esum2d  34095  voliune  34231  signsply0  34567  signstfvneq0  34588  f1o2d2  42274
  Copyright terms: Public domain W3C validator