Metamath Proof Explorer

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 φ ψ χ ↔ φ ∧ ψ