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 8201 ntrivcvgmul 15248 tsmsxp 22692 tgqioo 23337 ovolunlem2 24028 plyadd 24736 plymul 24737 coeeu 24744 tghilberti2 26352 nosupbnd1lem2 33107 btwnconn1lem2 33447 btwnconn1lem3 33448 btwnconn1lem12 33457 athgt 36474 2llnjN 36585 4atlem12b 36629 lncmp 36801 cdlema2N 36810 cdlemc2 37210 cdleme5 37258 cdleme11a 37278 cdleme21ct 37347 cdleme21 37355 cdleme22eALTN 37363 cdleme24 37370 cdleme27cl 37384 cdleme27a 37385 cdleme28 37391 cdleme36a 37478 cdleme42b 37496 cdleme48fvg 37518 cdlemf 37581 cdlemk39 37934 cdlemkid1 37940 dihlsscpre 38252 dihord4 38276 dihord5apre 38280 dihmeetlem20N 38344 mapdh9a 38807 pellex 39312 jm2.27 39485 |
Copyright terms: Public domain | W3C validator |