![]() |
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 1199 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant1 1130 | 1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: pceu 16841 axpasch 28870 3dimlem4 39174 3atlem4 39196 llncvrlpln2 39267 2lplnja 39329 lhpmcvr5N 39737 4atexlemswapqr 39773 4atexlemnclw 39780 trlval2 39873 cdleme21h 40044 cdleme24 40062 cdleme26ee 40070 cdleme26f 40073 cdleme26f2 40075 cdlemf1 40271 cdlemg16ALTN 40368 cdlemg17iqN 40384 cdlemg27b 40406 trlcone 40438 cdlemg48 40447 tendocan 40534 cdlemk26-3 40616 cdlemk27-3 40617 cdlemk28-3 40618 cdlemk37 40624 cdlemky 40636 cdlemk11ta 40639 cdlemkid3N 40643 cdlemk11t 40656 cdlemk46 40658 cdlemk47 40659 cdlemk51 40663 cdlemk52 40664 cdleml4N 40689 dihmeetlem1N 41000 dihmeetlem20N 41036 mapdpglem32 41415 addlimc 45303 iscnrm3rlem8 48315 |
Copyright terms: Public domain | W3C validator |