| 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 19034 neiptopnei 23057 neitx 23532 ustex3sym 24143 restutop 24163 ustuqtop4 24170 utopreg 24178 xrge0tsms 24761 noetainflem4 27690 f1otrg 28784 nn0xmulclb 32685 xrge0tsmsd 32993 elrgspnlem4 33177 imaslmod 33305 elrspunidl 33380 rhmpreimaprmidl 33403 qsidomlem1 33404 mxidlprm 33422 1arithidom 33489 dfufd2 33502 extdg1id 33642 pstmxmet 33857 esumfsup 34030 esum2dlem 34052 esum2d 34053 omssubadd 34261 eulerpartlemgvv 34337 signstfvneq0 34533 satffunlem2lem1 35355 matunitlindflem2 37570 aks6d1c2p2 42061 dffltz 42589 eldioph2 42717 limcrecl 45594 icccncfext 45852 ioodvbdlimc1lem2 45897 ioodvbdlimc2lem 45899 stoweidlem60 46025 fourierdlem77 46148 fourierdlem80 46151 fourierdlem103 46174 fourierdlem104 46175 etransclem35 46234 |
| Copyright terms: Public domain | W3C validator |