|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 3anassrs | Structured version Visualization version GIF version | ||
| Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.) | 
| Ref | Expression | 
|---|---|
| 3anassrs.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | 
| Ref | Expression | 
|---|---|
| 3anassrs | ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 3anassrs.1 | . . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | |
| 2 | 1 | 3exp2 1354 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | 
| 3 | 2 | imp41 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 |