Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp-6r | 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-6r | ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | 1 | ad6antlr 737 | 1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: catass 17060 mhmmnd 18339 scmatscm 21264 cfilucfil 23312 2sqmo 26173 istrkgb 26401 istrkge 26403 tgbtwnconn1 26521 legso 26545 footexALT 26664 opphl 26700 trgcopy 26750 dfcgra2 26776 cgrg3col4 26799 f1otrg 26817 2ndresdju 30560 cyc3genpm 30996 cyc3conja 31001 rhmimaidl 31181 ssmxidllem 31213 pstmxmet 31419 signstfvneq0 32121 afsval 32221 mblfinlem3 35439 mblfinlem4 35440 dffltz 40043 iunconnlem2 42093 suplesup 42416 limclner 42734 fourierdlem51 43240 hoidmvle 43680 smfmullem3 43866 |
Copyright terms: Public domain | W3C validator |