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 734 | 1 ⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: catass 17395 mhmmnd 18697 scmatscm 21662 cfilucfil 23715 2sqmo 26585 istrkgb 26816 istrkge 26818 tgbtwnconn1 26936 legso 26960 footexALT 27079 opphl 27115 trgcopy 27165 dfcgra2 27191 cgrg3col4 27214 f1otrg 27232 2ndresdju 30986 cyc3genpm 31419 cyc3conja 31424 rhmimaidl 31609 ssmxidllem 31641 pstmxmet 31847 signstfvneq0 32551 afsval 32651 mblfinlem3 35816 mblfinlem4 35817 dffltz 40471 iunconnlem2 42555 suplesup 42878 limclner 43192 fourierdlem51 43698 hoidmvle 44138 smfmullem3 44327 |
Copyright terms: Public domain | W3C validator |