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- ( 𝜓 , 𝜒 , 𝜒 ) )