![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp13r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp13r | ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1216 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant1 1124 | 1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 387 df-3an 1073 |
This theorem is referenced by: pceu 15955 axpasch 26290 3dimlem4 35613 3atlem4 35635 llncvrlpln2 35706 2lplnja 35768 lhpmcvr5N 36176 4atexlemswapqr 36212 4atexlemnclw 36219 trlval2 36312 cdleme21h 36483 cdleme24 36501 cdleme26ee 36509 cdleme26f 36512 cdleme26f2 36514 cdlemf1 36710 cdlemg16ALTN 36807 cdlemg17iqN 36823 cdlemg27b 36845 trlcone 36877 cdlemg48 36886 tendocan 36973 cdlemk26-3 37055 cdlemk27-3 37056 cdlemk28-3 37057 cdlemk37 37063 cdlemky 37075 cdlemk11ta 37078 cdlemkid3N 37082 cdlemk11t 37095 cdlemk46 37097 cdlemk47 37098 cdlemk51 37102 cdlemk52 37103 cdleml4N 37128 dihmeetlem1N 37439 dihmeetlem20N 37475 mapdpglem32 37854 addlimc 40781 |
Copyright terms: Public domain | W3C validator |