Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp3ll | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp3ll | ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll 765 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant3 1131 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: f1oiso2 7107 omeu 8213 ntrivcvgmul 15260 tsmsxp 22765 tgqioo 23410 ovolunlem2 24101 plyadd 24809 plymul 24810 coeeu 24817 tghilberti2 26426 nosupbnd1lem2 33211 btwnconn1lem2 33551 btwnconn1lem3 33552 btwnconn1lem12 33561 athgt 36594 2llnjN 36705 4atlem12b 36749 lncmp 36921 cdlema2N 36930 cdlemc2 37330 cdleme5 37378 cdleme11a 37398 cdleme21ct 37467 cdleme21 37475 cdleme22eALTN 37483 cdleme24 37490 cdleme27cl 37504 cdleme27a 37505 cdleme28 37511 cdleme36a 37598 cdleme42b 37616 cdleme48fvg 37638 cdlemf 37701 cdlemk39 38054 cdlemkid1 38060 dihlsscpre 38372 dihord4 38396 dihord5apre 38400 dihmeetlem20N 38464 mapdh9a 38927 pellex 39439 jm2.27 39612 |
Copyright terms: Public domain | W3C validator |