Metamath Proof Explorer


Theorem aprilfools2025

Description: An abuse of notation. (Contributed by Prof. Loof Lirpa, 1-Apr-2025) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion aprilfools2025 ⟨“ April ”⟩ ⟨“ fools! ”⟩ V

Proof

Step Hyp Ref Expression
1 s4cli ⟨“ ⟨“ ⟨“ Never ”⟩ ⟨“ gonna ”⟩ ⟨“ give ”⟩ ⟨“ you ”⟩ ⟨“ up ”⟩ ”⟩ ⟨“ ⟨“ Never ”⟩ ⟨“ gonna ”⟩ ⟨“ let ”⟩ ⟨“ you ”⟩ ⟨“ down ”⟩ ”⟩ ⟨“ ⟨“ Never ”⟩ ⟨“ gonna ”⟩ ⟨“ turn ”⟩ ⟨“ around ”⟩ ⟨“ and ”⟩ ”⟩ ⟨“ ⟨“ desert ”⟩ ⟨“ you! ”⟩ ”⟩ ”⟩ Word V
2 prex ⟨“ April ”⟩ ⟨“ fools! ”⟩ V
3 1 2 iddii ⟨“ April ”⟩ ⟨“ fools! ”⟩ V