Metamath Proof Explorer
Description: Theorem *2.24 of WhiteheadRussell p. 104. Its associated inference is
pm2.24i . Commuted form of pm2.21 . (Contributed by NM, 3Jan2005)


Ref 
Expression 

Assertion 
pm2.24 
$${\u22a2}{\phi}\to \left(\neg {\phi}\to {\psi}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

pm2.21 
$${\u22a2}\neg {\phi}\to \left({\phi}\to {\psi}\right)$$ 
2 
1

com12 
$${\u22a2}{\phi}\to \left(\neg {\phi}\to {\psi}\right)$$ 