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 737 | 1 ⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: catass 16957 2sqmo 26013 tgbtwnconn1 26361 legso 26385 miriso 26456 footexALT 26504 footex 26507 opphl 26540 lnopp2hpgb 26549 f1otrg 26657 cyc3genpm 30794 cyc3conja 30799 isprmidlc 30963 mxidlprm 30977 afsval 31942 dffltz 39291 smfmullem3 43088 |
Copyright terms: Public domain | W3C validator |