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.) |
Ref | Expression |
---|---|
simpl31 | ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp31 1090 | . 2 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | adantr 480 | 1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: ax5seglem3a 25610 ax5seg 25618 br8d 28802 br8 30899 cgrextend 31285 segconeq 31287 trisegint 31305 ifscgr 31321 cgrsub 31322 btwnxfr 31333 seglecgr12im 31387 segletr 31391 atbtwn 33750 3dim1 33771 2llnjaN 33870 4atlem10b 33909 4atlem11 33913 4atlem12 33916 2lplnj 33924 paddasslem4 34127 pmodlem1 34150 4atex2 34381 trlval3 34492 arglem1N 34495 cdleme0moN 34530 cdleme17b 34592 cdleme20 34630 cdleme21j 34642 cdleme28c 34678 cdleme35h2 34763 cdlemg6c 34926 cdlemg6 34929 cdlemg7N 34932 cdlemg8c 34935 cdlemg11a 34943 cdlemg11b 34948 cdlemg12e 34953 cdlemg16 34963 cdlemg16ALTN 34964 cdlemg16zz 34966 cdlemg20 34991 cdlemg22 34993 cdlemg37 34995 cdlemg31d 35006 cdlemg33b 35013 cdlemg33 35017 cdlemg39 35022 cdlemg42 35035 cdlemk25-3 35210 cdlemk33N 35215 cdlemk53b 35262 uhgr1wlkspth 40961 usgr2wlkspth 40965 |
Copyright terms: Public domain | W3C validator |