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 764 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant3 1134 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 |
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 397 df-3an 1088 |
This theorem is referenced by: f1oiso2 7223 omeu 8416 ntrivcvgmul 15614 tsmsxp 23306 tgqioo 23963 ovolunlem2 24662 plyadd 25378 plymul 25379 coeeu 25386 tghilberti2 26999 nosupbnd1lem2 33912 noinfbnd1lem2 33927 btwnconn1lem2 34390 btwnconn1lem3 34391 btwnconn1lem12 34400 athgt 37470 2llnjN 37581 4atlem12b 37625 lncmp 37797 cdlema2N 37806 cdlemc2 38206 cdleme5 38254 cdleme11a 38274 cdleme21ct 38343 cdleme21 38351 cdleme22eALTN 38359 cdleme24 38366 cdleme27cl 38380 cdleme27a 38381 cdleme28 38387 cdleme36a 38474 cdleme42b 38492 cdleme48fvg 38514 cdlemf 38577 cdlemk39 38930 cdlemkid1 38936 dihlsscpre 39248 dihord4 39272 dihord5apre 39276 dihmeetlem20N 39340 mapdh9a 39803 pellex 40657 jm2.27 40830 |
Copyright terms: Public domain | W3C validator |