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.) |
Ref | Expression |
---|---|
simp-5l | ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp-4l 802 | . 2 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | |
2 | 1 | adantr 480 | 1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 |
This theorem is referenced by: simp-6l 806 mhmmnd 17360 neiptopnei 20746 neitx 21220 ustex3sym 21831 restutop 21851 ustuqtop4 21858 utopreg 21866 xrge0tsms 22445 f1otrg 25551 usg2spot2nb 26592 xrge0tsmsd 29116 pstmxmet 29268 esumfsup 29459 esum2dlem 29481 esum2d 29482 omssubadd 29689 eulerpartlemgvv 29765 matunitlindflem2 32576 eldioph2 36343 limcrecl 38696 icccncfext 38773 ioodvbdlimc1lem2 38822 ioodvbdlimc2lem 38824 stoweidlem60 38953 fourierdlem77 39076 fourierdlem80 39079 fourierdlem103 39102 fourierdlem104 39103 etransclem35 39162 |
Copyright terms: Public domain | W3C validator |