Metamath Proof Explorer

Theorem ifpbi1b

Description: When the first variable is irrelevant, it can be replaced. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpbi1b ⊢ if- φ χ χ ↔ if- ψ χ χ

Proof

Step Hyp Ref Expression
1 id ⊢ χ → χ
2 1 olci ⊢ φ → ¬ ψ ∨ χ → χ
3 1 olci ⊢ ψ → φ ∨ χ → χ
4 2 3 pm3.2i ⊢ φ → ¬ ψ ∨ χ → χ ∧ ψ → φ ∨ χ → χ
5 1 olci ⊢ φ → ψ ∨ χ → χ
6 1 olci ⊢ ¬ ψ → φ ∨ χ → χ
7 5 6 pm3.2i ⊢ φ → ψ ∨ χ → χ ∧ ¬ ψ → φ ∨ χ → χ
8 ifpim123g ⊢ if- φ χ χ → if- ψ χ χ ↔ φ → ¬ ψ ∨ χ → χ ∧ ψ → φ ∨ χ → χ ∧ φ → ψ ∨ χ → χ ∧ ¬ ψ → φ ∨ χ → χ
9 4 7 8 mpbir2an ⊢ if- φ χ χ → if- ψ χ χ
10 1 olci ⊢ ψ → ¬ φ ∨ χ → χ
11 10 5 pm3.2i ⊢ ψ → ¬ φ ∨ χ → χ ∧ φ → ψ ∨ χ → χ
12 1 olci ⊢ ¬ φ → ψ ∨ χ → χ
13 3 12 pm3.2i ⊢ ψ → φ ∨ χ → χ ∧ ¬ φ → ψ ∨ χ → χ
14 ifpim123g ⊢ if- ψ χ χ → if- φ χ χ ↔ ψ → ¬ φ ∨ χ → χ ∧ φ → ψ ∨ χ → χ ∧ ψ → φ ∨ χ → χ ∧ ¬ φ → ψ ∨ χ → χ
15 11 13 14 mpbir2an ⊢ if- ψ χ χ → if- φ χ χ
16 9 15 impbii ⊢ if- φ χ χ ↔ if- ψ χ χ