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 ) ) )

Step	Hyp	Ref	Expression
1		simpl	\|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ph <-> ps ) )
2		simpr	\|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ch <-> th ) )
3	1 2	ifpbi23d	\|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ph <-> ps ) )

 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( ch <-> th ) )

1 2

 |-  ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> ( if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )