Metamath Proof Explorer

Theorem ifcomnan

Description: Commute the conditions in two nested conditionals if both conditions are not simultaneously true. (Contributed by SO, 15-Jul-2018)

Ref Expression
Assertion ifcomnan ⊢ ¬ φ ∧ ψ → if φ A if ψ B C = if ψ B if φ A C

Proof

Step Hyp Ref Expression
1 pm3.13 ⊢ ¬ φ ∧ ψ → ¬ φ ∨ ¬ ψ
2 iffalse ⊢ ¬ φ → if φ A if ψ B C = if ψ B C
3 iffalse ⊢ ¬ φ → if φ A C = C
4 3 ifeq2d ⊢ ¬ φ → if ψ B if φ A C = if ψ B C
5 2 4 eqtr4d ⊢ ¬ φ → if φ A if ψ B C = if ψ B if φ A C
6 iffalse ⊢ ¬ ψ → if ψ B C = C
7 6 ifeq2d ⊢ ¬ ψ → if φ A if ψ B C = if φ A C
8 iffalse ⊢ ¬ ψ → if ψ B if φ A C = if φ A C
9 7 8 eqtr4d ⊢ ¬ ψ → if φ A if ψ B C = if ψ B if φ A C
10 5 9 jaoi ⊢ ¬ φ ∨ ¬ ψ → if φ A if ψ B C = if ψ B if φ A C
11 1 10 syl ⊢ ¬ φ ∧ ψ → if φ A if ψ B C = if ψ B if φ A C