Metamath Proof Explorer

Theorem ifpid1g

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

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

Proof

Step Hyp Ref Expression
1 ifpidg 
 |-  ( ( ph <-> if- ( ph , ps , ch ) ) <-> ( ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) /\ ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) ) )
2 ancom 
 |-  ( ( ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) /\ ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) ) <-> ( ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) ) )
3 pm4.25 
 |-  ( ph <-> ( ph \/ ph ) )
4 3 imbi2i 
 |-  ( ( ch -> ph ) <-> ( ch -> ( ph \/ ph ) ) )
5 orc 
 |-  ( ph -> ( ph \/ ch ) )
6 5 biantru 
 |-  ( ( ch -> ( ph \/ ph ) ) <-> ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) )
7 4 6 bitr2i 
 |-  ( ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) <-> ( ch -> ph ) )
8 pm4.24 
 |-  ( ph <-> ( ph /\ ph ) )
9 8 imbi1i 
 |-  ( ( ph -> ps ) <-> ( ( ph /\ ph ) -> ps ) )
10 simpl 
 |-  ( ( ph /\ ps ) -> ph )
11 10 biantrur 
 |-  ( ( ( ph /\ ph ) -> ps ) <-> ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) )
12 9 11 bitr2i 
 |-  ( ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) <-> ( ph -> ps ) )
13 7 12 anbi12i 
 |-  ( ( ( ( ch -> ( ph \/ ph ) ) /\ ( ph -> ( ph \/ ch ) ) ) /\ ( ( ( ph /\ ps ) -> ph ) /\ ( ( ph /\ ph ) -> ps ) ) ) <-> ( ( ch -> ph ) /\ ( ph -> ps ) ) )
14 1 2 13 3bitri 
 |-  ( ( ph <-> if- ( ph , ps , ch ) ) <-> ( ( ch -> ph ) /\ ( ph -> ps ) ) )