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 767 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | |
2 | 1 | 3ad2ant3 1136 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 |
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 210 df-an 400 df-3an 1090 |
This theorem is referenced by: f1oiso2 7131 omeu 8255 ntrivcvgmul 15363 tsmsxp 22919 tgqioo 23565 ovolunlem2 24263 plyadd 24979 plymul 24980 coeeu 24987 tghilberti2 26597 nosupbnd1lem2 33568 noinfbnd1lem2 33583 btwnconn1lem2 34046 btwnconn1lem3 34047 btwnconn1lem12 34056 athgt 37126 2llnjN 37237 4atlem12b 37281 lncmp 37453 cdlema2N 37462 cdlemc2 37862 cdleme5 37910 cdleme11a 37930 cdleme21ct 37999 cdleme21 38007 cdleme22eALTN 38015 cdleme24 38022 cdleme27cl 38036 cdleme27a 38037 cdleme28 38043 cdleme36a 38130 cdleme42b 38148 cdleme48fvg 38170 cdlemf 38233 cdlemk39 38586 cdlemkid1 38592 dihlsscpre 38904 dihord4 38928 dihord5apre 38932 dihmeetlem20N 38996 mapdh9a 39459 pellex 40270 jm2.27 40443 |
Copyright terms: Public domain | W3C validator |