| 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 767 | . 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: tfrlem5 8420 omeu 8623 expmordi 14207 hash7g 14525 4sqlem18 17000 vdwlem10 17028 0catg 17731 mvrf1 22006 mdetuni0 22627 mdetmul 22629 tsmsxp 24163 ax5seglem3 28946 btwnconn1lem1 36088 btwnconn1lem2 36089 btwnconn1lem3 36090 btwnconn1lem12 36099 btwnconn1lem13 36100 lshpkrlem6 39116 athgt 39458 2llnjN 39569 dalaw 39888 lhpmcvr4N 40028 cdlemb2 40043 4atexlemex6 40076 cdlemd7 40206 cdleme01N 40223 cdleme02N 40224 cdleme0ex1N 40225 cdleme0ex2N 40226 cdleme7aa 40244 cdleme7c 40247 cdleme7d 40248 cdleme7e 40249 cdleme7ga 40250 cdleme7 40251 cdleme11a 40262 cdleme20k 40321 cdleme27cl 40368 cdleme42e 40481 cdleme42h 40484 cdleme42i 40485 cdlemf 40565 cdlemg2kq 40604 cdlemg2m 40606 cdlemg8a 40629 cdlemg11aq 40640 cdlemg10c 40641 cdlemg11b 40644 cdlemg17a 40663 cdlemg31b0N 40696 cdlemg31c 40701 cdlemg33c0 40704 cdlemg41 40720 cdlemh2 40818 cdlemn9 41207 dihglbcpreN 41302 dihmeetlem3N 41307 dihmeetlem13N 41321 pellex 42846 |
| Copyright terms: Public domain | W3C validator |