Theorem ifpxorxorb

Description: Factor conditional logic operator over xor in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

	Ref	Expression
Assertion	ifpxorxorb	|- ( if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> ( if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-xor	|- ( ( ps \/_ ch ) <-> -. ( ps <-> ch ) )
2		df-xor	|- ( ( th \/_ ta ) <-> -. ( th <-> ta ) )
3		ifpbi23	|- ( ( ( ( ps \/_ ch ) <-> -. ( ps <-> ch ) ) /\ ( ( th \/_ ta ) <-> -. ( th <-> ta ) ) ) -> ( if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> if- ( ph , -. ( ps <-> ch ) , -. ( th <-> ta ) ) ) )
4	1 2 3	mp2an	|- ( if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> if- ( ph , -. ( ps <-> ch ) , -. ( th <-> ta ) ) )
5		ifpbibib	|- ( if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
6	5	notbii	|- ( -. if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) <-> -. ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
7		ifpnotnotb	|- ( if- ( ph , -. ( ps <-> ch ) , -. ( th <-> ta ) ) <-> -. if- ( ph , ( ps <-> ch ) , ( th <-> ta ) ) )
8		df-xor	|- ( ( if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) <-> -. ( if- ( ph , ps , th ) <-> if- ( ph , ch , ta ) ) )
9	6 7 8	3bitr4i	|- ( if- ( ph , -. ( ps <-> ch ) , -. ( th <-> ta ) ) <-> ( if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) )
10	4 9	bitri	|- ( if- ( ph , ( ps \/_ ch ) , ( th \/_ ta ) ) <-> ( if- ( ph , ps , th ) \/_ if- ( ph , ch , ta ) ) )