# Some Practice Proofs 

Please Note: The rule "SI(X)" means that we would interpolate the
proof of the previous result by the name of "X".


P -> (Q <-> R) |- (P & Q) -> R 

1	(1) P -> (Q <-> R)	A 
2	(2) P & Q		A [goal: R]
2	(3) P			2 &E
1,2	(4) Q <-> R		1,3 ->E
1,2	(5) (Q -> R) & (R -> Q)	4 Df.<->
1,2	(6) Q -> R		5 &E
2	(7) Q			2 &E
1,2	(8) R			6,7 ->E
1	(9) (P & Q) -> R	2,8 ->I		


P -> (Q v R) |- P -> (Q v S)

1	(1) P -> (Q v R)	A
2	(2) R -> S		A
3	(3) P			A [goal: Q v S]
1,3	(4) Q v R		1,3 ->E
5	(5) Q			A
5	(6) Q v S		5 vI
7	(7) R			A
2,7	(8) S			2,7 ->E
2,7	(9) Q v S		8 vI
1,2,3	(10) Q v S		4,5,6,7,9 vE
1,2	(11) P -> (Q v S)	3,10 ->I


(P v Q) & (R v S) |- ((P & R) v (P & S)) v ((Q & R) v (Q & S))

1	(1) (P v Q) & (R v S)				A
1	(2) P v Q					1 &E
1	(3) R v S					1 &E
4	(4) P						A
5	(5) Q						A
6	(6) R						A
7	(7) S						A
4,6	(8) P & R					4,6 &I
4,6     (9) (P & R) v (P & S)				8 vI
4,6	(10) ((P & R) v (P & S)) v ((Q & R) v (Q & S))	9 vI
4,7	(11) P & S				   	4,7 &I
4,7	(12) (P & R) v (P & S)			 	11 vI
4,7	(13) ((P & R) v (P & S)) v ((Q & R) v (Q & S))	12 vI
1,4	(14) ((P & R) v (P & S)) v ((Q & R) v (Q & S))  3,6,10,7,13 vE
5,6	(15) Q & R				   	5,6 &I
5,6     (16) (Q & R) v (Q & S)			   	15 vI
5,6	(17) ((P & R) v (P & S)) v ((Q & R) v (Q & S))	16 vI
5,7	(18) Q & S				   	4,7 &I
5,7	(19) (Q & R) v (Q & S)			   	18 vI
5,7	(20) ((P & R) v (P & S)) v ((Q & R) v (Q & S))	19 vI
1,5	(21) ((P & R) v (P & S)) v ((Q & R) v (Q & S))  3,6,10,7,13 vE
1	(22) ((P & R) v (P & S)) v ((Q & R) v (Q & S))	2,4,14,5,21 vE


(P -> -Q) -> (R v S) |- (P & Q) v (-S -> R)

1	(1) (P -> -Q) -> (R v S)		A
1	(2) -(P -> -Q) v (R v S)		1 SI(Material Implication)
3	(3) -(P -> -Q) 	     			A
3	(4) P & --Q				3 SI(Material Implication)
3	(5) P 					4 &E
3	(6) --Q					4 &E
3	(7) Q					6 -E
3	(8) P & Q				5,7 &I
3	(9) (P & Q) v (-S -> R)			8 vI
10	(10) R v S    	     			A
11	(11) R 	 				A
11	(12) --S v R				11 vI
13	(13) S	   				A
13	(14) --S				13 -E
13	(15) --S v R				14 vI
10	(16) --S v R				10,11,12,13,15 vE
10	(17) -S -> R				16 SI(Material Implication)
10	(18) (P & Q) v (-S -> R)		17 vI
1	(19) (P & Q) v (-S -> R)		2,3,9,10,18 vE