Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl31 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpl31 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 1187 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑) | |
2 | 1 | 3ad2antl3 1183 | 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: ax5seglem3a 26715 ax5seg 26723 uhgrwkspth 27535 usgr2wlkspth 27539 br8d 30360 br8 32992 nosupres 33207 cgrextend 33469 segconeq 33471 trisegint 33489 ifscgr 33505 cgrsub 33506 btwnxfr 33517 seglecgr12im 33571 segletr 33575 atbtwn 36581 3dim1 36602 2llnjaN 36701 4atlem10b 36740 4atlem11 36744 4atlem12 36747 2lplnj 36755 paddasslem4 36958 pmodlem1 36981 4atex2 37212 trlval3 37322 arglem1N 37325 cdleme0moN 37360 cdleme17b 37422 cdleme20 37459 cdleme21j 37471 cdleme28c 37507 cdleme35h2 37592 cdlemg6c 37755 cdlemg6 37758 cdlemg7N 37761 cdlemg8c 37764 cdlemg11a 37772 cdlemg11b 37777 cdlemg12e 37782 cdlemg16 37792 cdlemg16ALTN 37793 cdlemg16zz 37795 cdlemg20 37820 cdlemg22 37822 cdlemg37 37824 cdlemg31d 37835 cdlemg33b 37842 cdlemg33 37846 cdlemg39 37851 cdlemg42 37864 cdlemk25-3 38039 cdlemk33N 38044 cdlemk53b 38091 |
Copyright terms: Public domain | W3C validator |