Metamath Proof Explorer

Theorem ifpid3g

Description: Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 olc 
 |-  ( ch -> ( ph \/ ch ) )
2 1 1 pm3.2i 
 |-  ( ( ch -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ch ) ) )
3 ifpidg 
 |-  ( ( ch <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> ch ) /\ ( ( ph /\ ch ) -> ps ) ) /\ ( ( ch -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ch ) ) ) ) )
4 2 3 mpbiran2 
 |-  ( ( ch <-> if- ( ph , ps , ch ) ) <-> ( ( ( ph /\ ps ) -> ch ) /\ ( ( ph /\ ch ) -> ps ) ) )