| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp3lr | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp3lr | ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simplr 769 | . 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 btwnconn1lem4 36091 athgt 39458 2llnjN 39569 4atlem12b 39613 lncmp 39785 cdlema2N 39794 cdleme21ct 40331 cdleme24 40354 cdleme27a 40369 cdleme28 40375 cdleme42b 40480 cdlemf 40565 dihlsscpre 41236 dihord4 41260 dihord5apre 41264 pellex 42846 jm2.27 43020 |
| Copyright terms: Public domain | W3C validator |