|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > simp3ll | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) | 
| Ref | Expression | 
|---|---|
| simp3ll | ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simpll 767 | . 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: f1oiso2 7372 omeu 8623 ntrivcvgmul 15938 tsmsxp 24163 tgqioo 24821 ovolunlem2 25533 plyadd 26256 plymul 26257 coeeu 26264 nosupbnd1lem2 27754 noinfbnd1lem2 27769 tghilberti2 28646 btwnconn1lem2 36089 btwnconn1lem3 36090 btwnconn1lem12 36099 athgt 39458 2llnjN 39569 4atlem12b 39613 lncmp 39785 cdlema2N 39794 cdlemc2 40194 cdleme5 40242 cdleme11a 40262 cdleme21ct 40331 cdleme21 40339 cdleme22eALTN 40347 cdleme24 40354 cdleme27cl 40368 cdleme27a 40369 cdleme28 40375 cdleme36a 40462 cdleme42b 40480 cdleme48fvg 40502 cdlemf 40565 cdlemk39 40918 cdlemkid1 40924 dihlsscpre 41236 dihord4 41260 dihord5apre 41264 dihmeetlem20N 41328 mapdh9a 41791 pellex 42846 jm2.27 43020 | 
| Copyright terms: Public domain | W3C validator |