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 763 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant3 1127 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: f1oiso2 7094 omeu 8200 ntrivcvgmul 15246 tsmsxp 22690 tgqioo 23335 ovolunlem2 24026 plyadd 24734 plymul 24735 coeeu 24742 tghilberti2 26351 nosupbnd1lem2 33106 btwnconn1lem2 33446 btwnconn1lem3 33447 btwnconn1lem12 33456 athgt 36472 2llnjN 36583 4atlem12b 36627 lncmp 36799 cdlema2N 36808 cdlemc2 37208 cdleme5 37256 cdleme11a 37276 cdleme21ct 37345 cdleme21 37353 cdleme22eALTN 37361 cdleme24 37368 cdleme27cl 37382 cdleme27a 37383 cdleme28 37389 cdleme36a 37476 cdleme42b 37494 cdleme48fvg 37516 cdlemf 37579 cdlemk39 37932 cdlemkid1 37938 dihlsscpre 38250 dihord4 38274 dihord5apre 38278 dihmeetlem20N 38342 mapdh9a 38805 pellex 39310 jm2.27 39483 |
Copyright terms: Public domain | W3C validator |