Metamath Proof Explorer

Theorem ifp1bi

Description: Substitute the first element of conditional logical operator. (Contributed by RP, 20-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 dfbi2 
 |-  ( ( if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) <-> ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) /\ ( if- ( ps , ch , th ) -> if- ( ph , ch , th ) ) ) )
2 ifpim1g 
 |-  ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ps -> ph ) \/ ( th -> ch ) ) /\ ( ( ph -> ps ) \/ ( ch -> th ) ) ) )
3 2 biancomi 
 |-  ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) <-> ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) )
4 ifpim1g 
 |-  ( ( if- ( ps , ch , th ) -> if- ( ph , ch , th ) ) <-> ( ( ( ph -> ps ) \/ ( th -> ch ) ) /\ ( ( ps -> ph ) \/ ( ch -> th ) ) ) )
5 3 4 anbi12i 
 |-  ( ( ( if- ( ph , ch , th ) -> if- ( ps , ch , th ) ) /\ ( if- ( ps , ch , th ) -> if- ( ph , ch , th ) ) ) <-> ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ps ) \/ ( th -> ch ) ) /\ ( ( ps -> ph ) \/ ( ch -> th ) ) ) ) )
6 an42 
 |-  ( ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) /\ ( ( ( ph -> ps ) \/ ( th -> ch ) ) /\ ( ( ps -> ph ) \/ ( ch -> th ) ) ) ) <-> ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ph -> ps ) \/ ( th -> ch ) ) ) /\ ( ( ( ps -> ph ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) ) )
7 1 5 6 3bitri 
 |-  ( ( if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) <-> ( ( ( ( ph -> ps ) \/ ( ch -> th ) ) /\ ( ( ph -> ps ) \/ ( th -> ch ) ) ) /\ ( ( ( ps -> ph ) \/ ( ch -> th ) ) /\ ( ( ps -> ph ) \/ ( th -> ch ) ) ) ) )