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 7105 omeu 8211 ntrivcvgmul 15258 tsmsxp 22763 tgqioo 23408 ovolunlem2 24099 plyadd 24807 plymul 24808 coeeu 24815 tghilberti2 26424 nosupbnd1lem2 33209 btwnconn1lem2 33549 btwnconn1lem3 33550 btwnconn1lem4 33551 athgt 36607 2llnjN 36718 4atlem12b 36762 lncmp 36934 cdlema2N 36943 cdleme21ct 37480 cdleme24 37503 cdleme27a 37518 cdleme28 37524 cdleme42b 37629 cdlemf 37714 dihlsscpre 38385 dihord4 38409 dihord5apre 38413 pellex 39452 jm2.27 39625 |
Copyright terms: Public domain | W3C validator |