|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp-8r | 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-8r | ⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
| 2 | 1 | ad8antlr 741 | 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: 2sqmo 27482 legso 28608 opphl 28763 f1otrg 28880 2ndresdju 32660 chnso 33005 cyc3conja 33178 rloccring 33275 ssdifidlprm 33487 mxidlprm 33499 mxidlirred 33501 constrconj 33787 constrfin 33788 constrelextdg2 33789 qtophaus 33836 esumcst 34065 dffltz 42649 smfmullem3 46813 | 
| Copyright terms: Public domain | W3C validator |