![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp2lr | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp2lr | ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simplr 769 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | |
2 | 1 | 3ad2ant2 1133 | 1 ⊢ ((𝜃 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: fpr3g 8309 tfrlem5 8419 omeu 8622 expmordi 14204 4sqlem18 16996 vdwlem10 17024 mvrf1 22024 mdetuni0 22643 mdetmul 22645 tsmsxp 24179 ax5seglem3 28961 btwnconn1lem1 36069 btwnconn1lem3 36071 btwnconn1lem4 36072 btwnconn1lem5 36073 btwnconn1lem6 36074 btwnconn1lem7 36075 linethru 36135 lshpkrlem6 39097 athgt 39439 2llnjN 39550 dalaw 39869 cdlemb2 40024 4atexlemex6 40057 cdleme01N 40204 cdleme0ex2N 40207 cdleme7aa 40225 cdleme7e 40230 cdlemg33c0 40685 dihmeetlem3N 41288 pellex 42823 |
Copyright terms: Public domain | W3C validator |