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 1083 | . 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓) | |
2 | 1 | 3ad2ant1 1075 | 1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: pceu 15389 axpasch 25621 3dimlem4 33768 3atlem4 33790 llncvrlpln2 33861 2lplnja 33923 lhpmcvr5N 34331 4atexlemswapqr 34367 4atexlemnclw 34374 trlval2 34468 cdleme21h 34640 cdleme24 34658 cdleme26ee 34666 cdleme26f 34669 cdleme26f2 34671 cdlemf1 34867 cdlemg16ALTN 34964 cdlemg17iqN 34980 cdlemg27b 35002 trlcone 35034 cdlemg48 35043 tendocan 35130 cdlemk26-3 35212 cdlemk27-3 35213 cdlemk28-3 35214 cdlemk37 35220 cdlemky 35232 cdlemk11ta 35235 cdlemkid3N 35239 cdlemk11t 35252 cdlemk46 35254 cdlemk47 35255 cdlemk51 35259 cdlemk52 35260 cdleml4N 35285 dihmeetlem1N 35597 dihmeetlem20N 35633 mapdpglem32 36012 addlimc 38715 |
Copyright terms: Public domain | W3C validator |