|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp33r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| simp33r | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp3r 1203 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant3 1136 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 | 
| 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 1089 | 
| This theorem is referenced by: totprob 34429 cdleme19b 40306 cdleme19e 40309 cdleme20h 40318 cdleme20l2 40323 cdleme20m 40325 cdleme21d 40332 cdleme21e 40333 cdleme22eALTN 40347 cdleme22f2 40349 cdleme22g 40350 cdleme26e 40361 cdleme37m 40464 cdlemeg46gfre 40534 cdlemg28a 40695 cdlemg28b 40705 cdlemk5a 40837 cdlemk6 40839 | 
| Copyright terms: Public domain | W3C validator |