![]() |
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 756 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant3 1115 | 1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 |
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 199 df-an 388 df-3an 1070 |
This theorem is referenced by: f1oiso2 6928 omeu 8012 ntrivcvgmul 15118 tsmsxp 22466 tgqioo 23111 ovolunlem2 23802 plyadd 24510 plymul 24511 coeeu 24518 tghilberti2 26126 nosupbnd1lem2 32727 btwnconn1lem2 33067 btwnconn1lem3 33068 btwnconn1lem4 33069 athgt 36034 2llnjN 36145 4atlem12b 36189 lncmp 36361 cdlema2N 36370 cdleme21ct 36907 cdleme24 36930 cdleme27a 36945 cdleme28 36951 cdleme42b 37056 cdlemf 37141 dihlsscpre 37812 dihord4 37836 dihord5apre 37840 pellex 38825 jm2.27 38998 |
Copyright terms: Public domain | W3C validator |