Metamath Proof Explorer

Theorem wl-ifp-ncond2

Description: If one case of an if- condition is false, the other automatically follows. (Contributed by Wolf Lammen, 21-Jul-2024)

Ref Expression
Assertion wl-ifp-ncond2 
|- ( -. ch -> ( if- ( ph , ps , ch ) <-> ( ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 wl-ifp-ncond1 
 |-  ( -. ch -> ( if- ( -. ph , ch , ps ) <-> ( -. -. ph /\ ps ) ) )
2 ifpn 
 |-  ( if- ( ph , ps , ch ) <-> if- ( -. ph , ch , ps ) )
3 notnotb 
 |-  ( ph <-> -. -. ph )
4 3 anbi1i 
 |-  ( ( ph /\ ps ) <-> ( -. -. ph /\ ps ) )
5 1 2 4 3bitr4g 
 |-  ( -. ch -> ( if- ( ph , ps , ch ) <-> ( ph /\ ps ) ) )