![]() |
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 1132 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: f1oiso2 7366 omeu 8617 ntrivcvgmul 15908 tsmsxp 24153 tgqioo 24810 ovolunlem2 25521 plyadd 26247 plymul 26248 coeeu 26255 nosupbnd1lem2 27742 noinfbnd1lem2 27757 tghilberti2 28568 btwnconn1lem2 35914 btwnconn1lem3 35915 btwnconn1lem4 35916 athgt 39157 2llnjN 39268 4atlem12b 39312 lncmp 39484 cdlema2N 39493 cdleme21ct 40030 cdleme24 40053 cdleme27a 40068 cdleme28 40074 cdleme42b 40179 cdlemf 40264 dihlsscpre 40935 dihord4 40959 dihord5apre 40963 pellex 42510 jm2.27 42684 |
Copyright terms: Public domain | W3C validator |