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

Theorem 3anassrs 1354
 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 1348 . 2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
32imp41 426 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1081 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 208  df-an 397  df-3an 1083 This theorem is referenced by:  ralrimivvva  3196  euotd  5399  dfgrp3e  18131  kerf1ghm  19419  kerf1hrmOLD  19420  psgndif  20664  neiptopnei  21658  neitr  21706  neitx  22133  cnextcn  22593  utoptop  22760  ustuqtoplem  22765  ustuqtop1  22767  utopsnneiplem  22773  utop3cls  22777  neipcfilu  22822  xmetpsmet  22875  metustsym  23082  grporcan  28211  disjdsct  30353  xrofsup  30407  omndmul2  30629  archirngz  30734  archiabllem1  30738  archiabllem2c  30740  reofld  30829  prmidl2  30866  pstmfval  31024  tpr2rico  31043  esumpcvgval  31225  esumcvg  31233  esum2d  31240  voliune  31376  signsply0  31709  signstfvneq0  31730
 Copyright terms: Public domain W3C validator