Metamath Proof Explorer

Theorem ifpbiidcor2

Description: Restatement of biid . (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpbiidcor2 
|- -. if- ( ph , -. ph , ph )

Proof

Step Hyp Ref Expression
1 ifpbiidcor 
 |-  if- ( ph , ph , -. ph )
2 ifpnot23b 
 |-  ( -. if- ( ph , -. ph , ph ) <-> if- ( ph , ph , -. ph ) )
3 1 2 mpbir 
 |-  -. if- ( ph , -. ph , ph )