Metamath Proof Explorer

Theorem ifpbi23

Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ph <-> ps ) )
2 1 imbi2d 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ta -> ph ) <-> ( ta -> ps ) ) )
3 simpr 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ch <-> th ) )
4 3 imbi2d 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( -. ta -> ch ) <-> ( -. ta -> th ) ) )
5 2 4 anbi12d 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ( ( ta -> ph ) /\ ( -. ta -> ch ) ) <-> ( ( ta -> ps ) /\ ( -. ta -> th ) ) ) )
6 dfifp2 
 |-  ( if- ( ta , ph , ch ) <-> ( ( ta -> ph ) /\ ( -. ta -> ch ) ) )
7 dfifp2 
 |-  ( if- ( ta , ps , th ) <-> ( ( ta -> ps ) /\ ( -. ta -> th ) ) )
8 5 6 7 3bitr4g 
 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )