| 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 1203 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
| 2 | 1 | 3ad2ant1 1134 | 1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: pceu 16884 axpasch 28956 3dimlem4 39466 3atlem4 39488 llncvrlpln2 39559 2lplnja 39621 lhpmcvr5N 40029 4atexlemswapqr 40065 4atexlemnclw 40072 trlval2 40165 cdleme21h 40336 cdleme24 40354 cdleme26ee 40362 cdleme26f 40365 cdleme26f2 40367 cdlemf1 40563 cdlemg16ALTN 40660 cdlemg17iqN 40676 cdlemg27b 40698 trlcone 40730 cdlemg48 40739 tendocan 40826 cdlemk26-3 40908 cdlemk27-3 40909 cdlemk28-3 40910 cdlemk37 40916 cdlemky 40928 cdlemk11ta 40931 cdlemkid3N 40935 cdlemk11t 40948 cdlemk46 40950 cdlemk47 40951 cdlemk51 40955 cdlemk52 40956 cdleml4N 40981 dihmeetlem1N 41292 dihmeetlem20N 41328 mapdpglem32 41707 addlimc 45663 iscnrm3rlem8 48844 |
| Copyright terms: Public domain | W3C validator |