|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simpr32 | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) | 
| Ref | Expression | 
|---|---|
| simpr32 | ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simpr2 1195 | . 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
| 2 | 1 | 3ad2antr3 1190 | 1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 | 
| 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 df-3an 1088 | 
| This theorem is referenced by: oppccatid 17763 subccatid 17892 fuccatid 18018 setccatid 18130 catccatid 18152 estrccatid 18177 xpccatid 18234 nllyidm 23498 utoptop 24244 omndmul2 33090 cgr3tr4 36054 paddasslem9 39831 cdlemd1 40201 cdlemf2 40565 cdlemk34 40913 dihmeetlem18N 41327 isthincd2 49111 mndtccatid 49239 | 
| Copyright terms: Public domain | W3C validator |