Theorem ifpananb

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

	Ref	Expression
Assertion	ifpananb	⊢ ( if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		anor	⊢ ( ( 𝜓 ∧ 𝜒 ) ↔ ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) )
2		anor	⊢ ( ( 𝜃 ∧ 𝜏 ) ↔ ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) )
3		ifpbi23	⊢ ( ( ( ( 𝜓 ∧ 𝜒 ) ↔ ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) ) ∧ ( ( 𝜃 ∧ 𝜏 ) ↔ ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ) → ( if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ) )
4	1 2 3	mp2an	⊢ ( if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) )
5		ifpororb	⊢ ( if- ( 𝜑 , ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ↔ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) ) )
6		ifpnotnotb	⊢ ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ↔ ¬ if- ( 𝜑 , 𝜓 , 𝜃 ) )
7		ifpnotnotb	⊢ ( if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) ↔ ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) )
8	6 7	orbi12i	⊢ ( ( if- ( 𝜑 , ¬ 𝜓 , ¬ 𝜃 ) ∨ if- ( 𝜑 , ¬ 𝜒 , ¬ 𝜏 ) ) ↔ ( ¬ if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
9	5 8	bitri	⊢ ( if- ( 𝜑 , ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ↔ ( ¬ if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
10	9	notbii	⊢ ( ¬ if- ( 𝜑 , ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ↔ ¬ ( ¬ if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
11		ifpnotnotb	⊢ ( if- ( 𝜑 , ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ↔ ¬ if- ( 𝜑 , ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) )
12		anor	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ¬ ( ¬ if- ( 𝜑 , 𝜓 , 𝜃 ) ∨ ¬ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
13	10 11 12	3bitr4i	⊢ ( if- ( 𝜑 , ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) , ¬ ( ¬ 𝜃 ∨ ¬ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
14	4 13	bitri	⊢ ( if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )