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 1204 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant1 1135 | 1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 |
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 210 df-an 400 df-3an 1091 |
This theorem is referenced by: pceu 16431 axpasch 27063 3dimlem4 37251 3atlem4 37273 llncvrlpln2 37344 2lplnja 37406 lhpmcvr5N 37814 4atexlemswapqr 37850 4atexlemnclw 37857 trlval2 37950 cdleme21h 38121 cdleme24 38139 cdleme26ee 38147 cdleme26f 38150 cdleme26f2 38152 cdlemf1 38348 cdlemg16ALTN 38445 cdlemg17iqN 38461 cdlemg27b 38483 trlcone 38515 cdlemg48 38524 tendocan 38611 cdlemk26-3 38693 cdlemk27-3 38694 cdlemk28-3 38695 cdlemk37 38701 cdlemky 38713 cdlemk11ta 38716 cdlemkid3N 38720 cdlemk11t 38733 cdlemk46 38735 cdlemk47 38736 cdlemk51 38740 cdlemk52 38741 cdleml4N 38766 dihmeetlem1N 39077 dihmeetlem20N 39113 mapdpglem32 39492 addlimc 42909 iscnrm3rlem8 45959 |
Copyright terms: Public domain | W3C validator |