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-ψχχ