Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp2ll | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2ll | ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 763 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant2 1132 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 1087 |
This theorem is referenced by: tfrlem5 8195 omeu 8392 expmordi 13866 4sqlem18 16644 vdwlem10 16672 0catg 17378 mvrf1 21175 mdetuni0 21751 mdetmul 21753 tsmsxp 23287 ax5seglem3 27280 btwnconn1lem1 34368 btwnconn1lem2 34369 btwnconn1lem3 34370 btwnconn1lem12 34379 btwnconn1lem13 34380 lshpkrlem6 37108 athgt 37449 2llnjN 37560 dalaw 37879 lhpmcvr4N 38019 cdlemb2 38034 4atexlemex6 38067 cdlemd7 38197 cdleme01N 38214 cdleme02N 38215 cdleme0ex1N 38216 cdleme0ex2N 38217 cdleme7aa 38235 cdleme7c 38238 cdleme7d 38239 cdleme7e 38240 cdleme7ga 38241 cdleme7 38242 cdleme11a 38253 cdleme20k 38312 cdleme27cl 38359 cdleme42e 38472 cdleme42h 38475 cdleme42i 38476 cdlemf 38556 cdlemg2kq 38595 cdlemg2m 38597 cdlemg8a 38620 cdlemg11aq 38631 cdlemg10c 38632 cdlemg11b 38635 cdlemg17a 38654 cdlemg31b0N 38687 cdlemg31c 38692 cdlemg33c0 38695 cdlemg41 38711 cdlemh2 38809 cdlemn9 39198 dihglbcpreN 39293 dihmeetlem3N 39298 dihmeetlem13N 39312 pellex 40637 |
Copyright terms: Public domain | W3C validator |