Step
*
1
1
1
1
of Lemma
logic6_contrapos
1. [P] : 
2. [Q] : 
3. P 
 Q@i
4. 
Q@i
5. P@i
 False
BY
{ Unfold `not` 4 }
1
1. [P] : 
2. [Q] : 
3. P 
 Q@i
4. Q 
 False@i
5. P@i
 False
1.  [P]  :  \mBbbP{}
2.  [Q]  :  \mBbbP{}
3.  P  {}\mRightarrow{}  Q@i
4.  \mneg{}Q@i
5.  P@i
\mvdash{}  False
By
Unfold  `not`  4
Home
Index