| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp-5l | Structured version Visualization version GIF version | ||
| Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
| Ref | Expression |
|---|---|
| simp-5l | ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
| 2 | 1 | ad5antr 734 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: mhmmnd 19082 neiptopnei 23140 neitx 23615 ustex3sym 24226 restutop 24246 ustuqtop4 24253 utopreg 24261 xrge0tsms 24856 noetainflem4 27785 f1otrg 28879 nn0xmulclb 32775 xrge0tsmsd 33065 elrgspnlem4 33249 imaslmod 33381 elrspunidl 33456 rhmpreimaprmidl 33479 qsidomlem1 33480 mxidlprm 33498 1arithidom 33565 dfufd2 33578 extdg1id 33716 pstmxmet 33896 esumfsup 34071 esum2dlem 34093 esum2d 34094 omssubadd 34302 eulerpartlemgvv 34378 signstfvneq0 34587 satffunlem2lem1 35409 matunitlindflem2 37624 aks6d1c2p2 42120 dffltz 42644 eldioph2 42773 limcrecl 45644 icccncfext 45902 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 stoweidlem60 46075 fourierdlem77 46198 fourierdlem80 46201 fourierdlem103 46224 fourierdlem104 46225 etransclem35 46284 |
| Copyright terms: Public domain | W3C validator |