Metamath Proof Explorer

Theorem ifpid2g

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

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

Proof

Step Hyp Ref Expression
1 ifpidg 
 |-  ( ( ps <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> ps ) /\ ( ( ph /\ ps ) -> ps ) ) /\ ( ( ch -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ch ) ) ) ) )
2 simpr 
 |-  ( ( ph /\ ps ) -> ps )
3 2 2 pm3.2i 
 |-  ( ( ( ph /\ ps ) -> ps ) /\ ( ( ph /\ ps ) -> ps ) )
4 3 biantrur 
 |-  ( ( ( ch -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ch ) ) ) <-> ( ( ( ( ph /\ ps ) -> ps ) /\ ( ( ph /\ ps ) -> ps ) ) /\ ( ( ch -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ch ) ) ) ) )
5 ancom 
 |-  ( ( ( ch -> ( ph \/ ps ) ) /\ ( ps -> ( ph \/ ch ) ) ) <-> ( ( ps -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ps ) ) ) )
6 1 4 5 3bitr2i 
 |-  ( ( ps <-> if- ( ph , ps , ch ) ) <-> ( ( ps -> ( ph \/ ch ) ) /\ ( ch -> ( ph \/ ps ) ) ) )