Home Metamath Proof ExplorerTheorem List (p. 354 of 370) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-25511) Hilbert Space Explorer (25512-27036) Users' Mathboxes (27037-36923)

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdleme46fsvlpq 35301* Show that is under when is. (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg46fvcl 35302* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme4gfv 35303* Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 35237? TODO: Can this be used to help prove the or case where is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 35289 help? (Contributed by NM, 8-Apr-2013.)

Theoremcdlemeg47b 35304* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg47rv 35305* Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg47rv2 35306* Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg49le 35307* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 9-Apr-2013.)

Theoremcdlemeg46bOLDN 35308* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46c 35309* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg46rvOLDN 35310* Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 3-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46rv2OLDN 35311* Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 3-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46fvaw 35312* Show that is an atom not under when is an atom not under . (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg46nlpq 35313* Show that is not under when isn't. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46ngfr 35314* TODO FIX COMMENT g(f(s))=s p. 115 4th line from bottom. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46nfgr 35315* TODO FIX COMMENT f(g(s))=s p. 115 antepenultimate line. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46sfg 35316* TODO FIX COMMENT f(r) s = f(r) g(s) p. 116 2nd line TODO: eliminate eqcomd? (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46fjgN 35317* NOT NEEDED? TODO FIX COMMENT TODO eliminate eqcomd 2475? p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46rjgN 35318* NOT NEEDED? TODO FIX COMMENT r g(s) = r v2 p. 115 last line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46fjv 35319* TODO FIX COMMENT f(r) f(g(s)) = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46fsfv 35320* TODO FIX COMMENT f(r) s = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46frv 35321* TODO FIX COMMENT (f(r) v2) w = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46v1v2 35322* TODO FIX COMMENT v1 = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46vrg 35323* TODO FIX COMMENT v1 r g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46rgv 35324* TODO FIX COMMENT r g(s) v1 p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46req 35325* TODO FIX COMMENT r = (v1 g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46gfv 35326* TODO FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1) (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gfr 35327* TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gfre 35328* TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gf 35329* TODO FIX COMMENT Eliminate antecedent . (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46fgN 35330* TODO FIX COMMENT p. 116 penultimate line: f(g(r)) = r. (Contributed by NM, 4-Apr-2013.) (New usage is discouraged.)

Theoremcdleme48d 35331* TODO: fix comment. (Contributed by NM, 8-Apr-2013.)

Theoremcdleme48gfv1 35332* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme48gfv 35333* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme48fgv 35334* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdlemeg49lebilem 35335* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50lebi 35336* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50eq 35337* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)