Re: [Metamath] ?Statement "a3" cannot be unified with step 25.

2023-08-13 Thread Mario Carneiro
axiom a3 is missing parentheses around it On Sun, Aug 13, 2023 at 5:30 PM Jeroen van Rensen wrote: > Hello everyone, > > I am trying to prove the following statement: > > ! ! p |- p > > The formal proof is as follows (the axioms are the same as in set.mm): > > 1. ! ! p (Premiss) > 2. ! ! p ->

[Metamath] ?Statement "a3" cannot be unified with step 25.

2023-08-13 Thread Jeroen van Rensen
Hello everyone, I am trying to prove the following statement: ! ! p |- p The formal proof is as follows (the axioms are the same as in set.mm): 1. ! ! p (Premiss) 2. ! ! p -> (! ! ! ! p -> ! ! p) (Axiom 1) 3. ! ! ! ! p -> ! ! p (MP 1, 2) 4. (! ! ! ! p -> ! ! p) -> (! p -> ! ! ! p) (Axiom 3) 5.