![]() |
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 733 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: mhmmnd 18874 neiptopnei 22499 neitx 22974 ustex3sym 23585 restutop 23605 ustuqtop4 23612 utopreg 23620 xrge0tsms 24213 noetainflem4 27104 f1otrg 27855 nn0xmulclb 31723 xrge0tsmsd 31948 imaslmod 32192 elrspunidl 32251 rhmpreimaprmidl 32272 qsidomlem1 32273 mxidlprm 32285 extdg1id 32409 pstmxmet 32535 esumfsup 32726 esum2dlem 32748 esum2d 32749 omssubadd 32957 eulerpartlemgvv 33033 signstfvneq0 33241 satffunlem2lem1 34055 matunitlindflem2 36121 aks6d1c2p2 40595 dffltz 41015 eldioph2 41128 limcrecl 43956 icccncfext 44214 ioodvbdlimc1lem2 44259 ioodvbdlimc2lem 44261 stoweidlem60 44387 fourierdlem77 44510 fourierdlem80 44513 fourierdlem103 44536 fourierdlem104 44537 etransclem35 44596 |
Copyright terms: Public domain | W3C validator |