![]() |
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 766 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 1131 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1084 |
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 206 df-an 396 df-3an 1086 |
This theorem is referenced by: fpr3g 8271 tfrlem5 8381 omeu 8586 expmordi 14137 4sqlem18 16904 vdwlem10 16932 mvrf1 21887 mdetuni0 22478 mdetmul 22480 tsmsxp 24014 ax5seglem3 28697 btwnconn1lem1 35592 btwnconn1lem3 35594 btwnconn1lem4 35595 btwnconn1lem5 35596 btwnconn1lem6 35597 btwnconn1lem7 35598 linethru 35658 lshpkrlem6 38498 athgt 38840 2llnjN 38951 dalaw 39270 cdlemb2 39425 4atexlemex6 39458 cdleme01N 39605 cdleme0ex2N 39608 cdleme7aa 39626 cdleme7e 39631 cdlemg33c0 40086 dihmeetlem3N 40689 pellex 42156 |
Copyright terms: Public domain | W3C validator |