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 730 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mhmmnd 18159 neiptopnei 21668 neitx 22143 ustex3sym 22753 restutop 22773 ustuqtop4 22780 utopreg 22788 xrge0tsms 23369 f1otrg 26584 nn0xmulclb 30422 xrge0tsmsd 30619 imaslmod 30849 qsidomlem1 30882 extdg1id 30952 pstmxmet 31036 esumfsup 31228 esum2dlem 31250 esum2d 31251 omssubadd 31457 eulerpartlemgvv 31533 signstfvneq0 31741 satffunlem2lem1 32548 matunitlindflem2 34770 dffltz 39149 eldioph2 39237 limcrecl 41786 icccncfext 42046 ioodvbdlimc1lem2 42093 ioodvbdlimc2lem 42095 stoweidlem60 42222 fourierdlem77 42345 fourierdlem80 42348 fourierdlem103 42371 fourierdlem104 42372 etransclem35 42431 |
Copyright terms: Public domain | W3C validator |