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- ( ph , ch , ch ) <-> if- ( ps , ch , ch ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ch -> ch )
2 1 olci 
 |-  ( ( ph -> -. ps ) \/ ( ch -> ch ) )
3 1 olci 
 |-  ( ( ps -> ph ) \/ ( ch -> ch ) )
4 2 3 pm3.2i 
 |-  ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( ch -> ch ) ) )
5 1 olci 
 |-  ( ( ph -> ps ) \/ ( ch -> ch ) )
6 1 olci 
 |-  ( ( -. ps -> ph ) \/ ( ch -> ch ) )
7 5 6 pm3.2i 
 |-  ( ( ( ph -> ps ) \/ ( ch -> ch ) ) /\ ( ( -. ps -> ph ) \/ ( ch -> ch ) ) )
8 ifpim123g 
 |-  ( ( if- ( ph , ch , ch ) -> if- ( ps , ch , ch ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( ch -> ch ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> ch ) ) /\ ( ( -. ps -> ph ) \/ ( ch -> ch ) ) ) ) )
9 4 7 8 mpbir2an 
 |-  ( if- ( ph , ch , ch ) -> if- ( ps , ch , ch ) )
10 1 olci 
 |-  ( ( ps -> -. ph ) \/ ( ch -> ch ) )
11 10 5 pm3.2i 
 |-  ( ( ( ps -> -. ph ) \/ ( ch -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> ch ) ) )
12 1 olci 
 |-  ( ( -. ph -> ps ) \/ ( ch -> ch ) )
13 3 12 pm3.2i 
 |-  ( ( ( ps -> ph ) \/ ( ch -> ch ) ) /\ ( ( -. ph -> ps ) \/ ( ch -> ch ) ) )
14 ifpim123g 
 |-  ( ( if- ( ps , ch , ch ) -> if- ( ph , ch , ch ) ) <-> ( ( ( ( ps -> -. ph ) \/ ( ch -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> ch ) ) ) /\ ( ( ( ps -> ph ) \/ ( ch -> ch ) ) /\ ( ( -. ph -> ps ) \/ ( ch -> ch ) ) ) ) )
15 11 13 14 mpbir2an 
 |-  ( if- ( ps , ch , ch ) -> if- ( ph , ch , ch ) )
16 9 15 impbii 
 |-  ( if- ( ph , ch , ch ) <-> if- ( ps , ch , ch ) )