Metamath Proof Explorer

Theorem ifpancor

Description: Corollary of commutation of and. (Contributed by RP, 25-Apr-2020)

Ref Expression
Assertion ifpancor 
|- ( if- ( ph , ps , ph ) <-> if- ( ps , ph , ps ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2 ifpdfan2 
 |-  ( ( ph /\ ps ) <-> if- ( ph , ps , ph ) )
3 ifpdfan2 
 |-  ( ( ps /\ ph ) <-> if- ( ps , ph , ps ) )
4 1 2 3 3bitr3i 
 |-  ( if- ( ph , ps , ph ) <-> if- ( ps , ph , ps ) )