![]() |
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 807 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant2 1129 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: tfrlem5 7641 omeu 7830 4sqlem18 15864 vdwlem10 15892 0catg 16545 mvrf1 19623 mdetuni0 20625 mdetmul 20627 tsmsxp 22155 ax5seglem3 26006 btwnconn1lem1 32496 btwnconn1lem2 32497 btwnconn1lem3 32498 btwnconn1lem12 32507 btwnconn1lem13 32508 lshpkrlem6 34901 athgt 35241 2llnjN 35352 dalaw 35671 lhpmcvr4N 35811 cdlemb2 35826 4atexlemex6 35859 cdlemd7 35990 cdleme01N 36007 cdleme02N 36008 cdleme0ex1N 36009 cdleme0ex2N 36010 cdleme7aa 36028 cdleme7c 36031 cdleme7d 36032 cdleme7e 36033 cdleme7ga 36034 cdleme7 36035 cdleme11a 36046 cdleme20k 36105 cdleme27cl 36152 cdleme42e 36265 cdleme42h 36268 cdleme42i 36269 cdlemf 36349 cdlemg2kq 36388 cdlemg2m 36390 cdlemg8a 36413 cdlemg11aq 36424 cdlemg10c 36425 cdlemg11b 36428 cdlemg17a 36447 cdlemg31b0N 36480 cdlemg31c 36485 cdlemg33c0 36488 cdlemg41 36504 cdlemh2 36602 cdlemn9 36992 dihglbcpreN 37087 dihmeetlem3N 37092 dihmeetlem13N 37106 pellex 37897 expmordi 38010 |
Copyright terms: Public domain | W3C validator |