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 767 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant3 1131 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: f1oiso2 7107 omeu 8213 ntrivcvgmul 15260 tsmsxp 22765 tgqioo 23410 ovolunlem2 24101 plyadd 24809 plymul 24810 coeeu 24817 tghilberti2 26426 nosupbnd1lem2 33211 btwnconn1lem2 33551 btwnconn1lem3 33552 btwnconn1lem4 33553 athgt 36594 2llnjN 36705 4atlem12b 36749 lncmp 36921 cdlema2N 36930 cdleme21ct 37467 cdleme24 37490 cdleme27a 37505 cdleme28 37511 cdleme42b 37616 cdlemf 37701 dihlsscpre 38372 dihord4 38396 dihord5apre 38400 pellex 39439 jm2.27 39612 |
Copyright terms: Public domain | W3C validator |