Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp2lr | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2lr | ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr 788 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 1076 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: tfrlem5 7363 omeu 7552 4sqlem18 15504 vdwlem10 15532 mvrf1 19246 mdetuni0 20246 mdetmul 20248 tsmsxp 21768 ax5seglem3 25611 btwnconn1lem1 31364 btwnconn1lem3 31366 btwnconn1lem4 31367 btwnconn1lem5 31368 btwnconn1lem6 31369 btwnconn1lem7 31370 linethru 31430 lshpkrlem6 33420 athgt 33760 2llnjN 33871 dalaw 34190 cdlemb2 34345 4atexlemex6 34378 cdleme01N 34526 cdleme0ex2N 34529 cdleme7aa 34547 cdleme7e 34552 cdlemg33c0 35008 dihmeetlem3N 35612 pellex 36417 expmordi 36530 |
Copyright terms: Public domain | W3C validator |