|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp33l | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| simp33l | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simp3l 1202 | . 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 cdleme19d 40308 cdleme19e 40309 cdleme20h 40318 cdleme20l2 40323 cdleme20m 40325 cdleme21d 40332 cdleme21e 40333 cdleme22e 40346 cdleme22f2 40349 cdleme22g 40350 cdleme26e 40361 cdleme28a 40372 cdleme28b 40373 cdleme37m 40464 cdleme39n 40468 cdlemeg46gfre 40534 cdlemg28a 40695 cdlemg28b 40705 cdlemk3 40835 cdlemk5a 40837 cdlemk6 40839 cdlemkuat 40868 cdlemkid2 40926 | 
| Copyright terms: Public domain | W3C validator |