| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp-7r | 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-7r | ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
| 2 | 1 | ad7antlr 739 | 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: catass 17609 2sqmo 27404 tgbtwnconn1 28647 legso 28671 miriso 28742 footexALT 28790 footex 28793 opphl 28826 lnopp2hpgb 28835 f1otrg 28943 2ndresdju 32727 cyc3genpm 33234 cyc3conja 33239 rloccring 33352 isprmidlc 33528 ssdifidlprm 33539 mxidlprm 33551 qsdrngi 33576 1arithidom 33618 fldext2chn 33885 constrconj 33902 constrfin 33903 constrelextdg2 33904 zarcmplem 34038 afsval 34828 dffltz 42877 smfmullem3 47037 chnerlem1 47126 |
| Copyright terms: Public domain | W3C validator |