Theorem cad0OLD

Description: Obsolete version of cad0 as of 21-Sep-2024. (Contributed by Mario Carneiro, 8-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cad0OLD	⊢ ( ¬ 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-cad	⊢ ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )
2		idd	⊢ ( ¬ 𝜒 → ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ 𝜓 ) ) )
3		pm2.21	⊢ ( ¬ 𝜒 → ( 𝜒 → ( 𝜑 ∧ 𝜓 ) ) )
4	3	adantrd	⊢ ( ¬ 𝜒 → ( ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) → ( 𝜑 ∧ 𝜓 ) ) )
5	2 4	jaod	⊢ ( ¬ 𝜒 → ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) → ( 𝜑 ∧ 𝜓 ) ) )
6		orc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) )
7	5 6	impbid1	⊢ ( ¬ 𝜒 → ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜒 ∧ ( 𝜑 ⊻ 𝜓 ) ) ) ↔ ( 𝜑 ∧ 𝜓 ) ) )
8	1 7	syl5bb	⊢ ( ¬ 𝜒 → ( cadd ( 𝜑 , 𝜓 , 𝜒 ) ↔ ( 𝜑 ∧ 𝜓 ) ) )