Theorem ifpnannanb

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

	Ref	Expression
Assertion	ifpnannanb	⊢ ( if- ( 𝜑 , ( 𝜓 ⊼ 𝜒 ) , ( 𝜃 ⊼ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊼ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-nan	⊢ ( ( 𝜓 ⊼ 𝜒 ) ↔ ¬ ( 𝜓 ∧ 𝜒 ) )
2		df-nan	⊢ ( ( 𝜃 ⊼ 𝜏 ) ↔ ¬ ( 𝜃 ∧ 𝜏 ) )
3		ifpbi23	⊢ ( ( ( ( 𝜓 ⊼ 𝜒 ) ↔ ¬ ( 𝜓 ∧ 𝜒 ) ) ∧ ( ( 𝜃 ⊼ 𝜏 ) ↔ ¬ ( 𝜃 ∧ 𝜏 ) ) ) → ( if- ( 𝜑 , ( 𝜓 ⊼ 𝜒 ) , ( 𝜃 ⊼ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( 𝜓 ∧ 𝜒 ) , ¬ ( 𝜃 ∧ 𝜏 ) ) ) )
4	1 2 3	mp2an	⊢ ( if- ( 𝜑 , ( 𝜓 ⊼ 𝜒 ) , ( 𝜃 ⊼ 𝜏 ) ) ↔ if- ( 𝜑 , ¬ ( 𝜓 ∧ 𝜒 ) , ¬ ( 𝜃 ∧ 𝜏 ) ) )
5		ifpananb	⊢ ( if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
6	5	notbii	⊢ ( ¬ if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) ↔ ¬ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
7		ifpnotnotb	⊢ ( if- ( 𝜑 , ¬ ( 𝜓 ∧ 𝜒 ) , ¬ ( 𝜃 ∧ 𝜏 ) ) ↔ ¬ if- ( 𝜑 , ( 𝜓 ∧ 𝜒 ) , ( 𝜃 ∧ 𝜏 ) ) )
8		df-nan	⊢ ( ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊼ if- ( 𝜑 , 𝜒 , 𝜏 ) ) ↔ ¬ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ∧ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
9	6 7 8	3bitr4i	⊢ ( if- ( 𝜑 , ¬ ( 𝜓 ∧ 𝜒 ) , ¬ ( 𝜃 ∧ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊼ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )
10	4 9	bitri	⊢ ( if- ( 𝜑 , ( 𝜓 ⊼ 𝜒 ) , ( 𝜃 ⊼ 𝜏 ) ) ↔ ( if- ( 𝜑 , 𝜓 , 𝜃 ) ⊼ if- ( 𝜑 , 𝜒 , 𝜏 ) ) )