| 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 769 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
| 2 | 1 | 3ad2ant2 1135 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: fpr3g 8310 tfrlem5 8420 omeu 8623 expmordi 14207 4sqlem18 17000 vdwlem10 17028 mvrf1 22006 mdetuni0 22627 mdetmul 22629 tsmsxp 24163 ax5seglem3 28946 btwnconn1lem1 36088 btwnconn1lem3 36090 btwnconn1lem4 36091 btwnconn1lem5 36092 btwnconn1lem6 36093 btwnconn1lem7 36094 linethru 36154 lshpkrlem6 39116 athgt 39458 2llnjN 39569 dalaw 39888 cdlemb2 40043 4atexlemex6 40076 cdleme01N 40223 cdleme0ex2N 40226 cdleme7aa 40244 cdleme7e 40249 cdlemg33c0 40704 dihmeetlem3N 41307 pellex 42846 |
| Copyright terms: Public domain | W3C validator |