Metamath Proof Explorer

Theorem ifpim1g

Description: Implication of conditional logical operators. (Contributed by RP, 18-Apr-2020)

Ref Expression
Assertion ifpim1g 
|- ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )

Proof

Step Hyp Ref Expression
1 ifpim123g 
 |-  ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( -. ps -> ph ) \/ ( th -> th ) ) ) ) )
2 id 
 |-  ( ch -> ch )
3 2 olci 
 |-  ( ( ph -> -. ps ) \/ ( ch -> ch ) )
4 3 biantrur 
 |-  ( ( ( ps -> ph ) \/ ( th -> ch ) ) <-> ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) )
5 4 bicomi 
 |-  ( ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) <-> ( ( ps -> ph ) \/ ( th -> ch ) ) )
6 id 
 |-  ( th -> th )
7 6 olci 
 |-  ( ( -. ps -> ph ) \/ ( th -> th ) )
8 7 biantru 
 |-  ( ( ( ph -> ps ) \/ ( ch -> th ) ) <-> ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( -. ps -> ph ) \/ ( th -> th ) ) ) )
9 8 bicomi 
 |-  ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( -. ps -> ph ) \/ ( th -> th ) ) ) <-> ( ( ph -> ps ) \/ ( ch -> th ) ) )
10 5 9 anbi12i 
 |-  ( ( ( ( ( ph -> -. ps ) \/ ( ch -> ch ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( -. ps -> ph ) \/ ( th -> th ) ) ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )
11 1 10 bitri 
 |-  ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )