Metamath Proof Explorer

Theorem ifpdfan

Description: Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020)

Ref Expression
Assertion ifpdfan 
|- ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )

Proof

Step Hyp Ref Expression
1 fal 
 |-  -. F.
2 1 intnan 
 |-  -. ( -. ph /\ F. )
3 2 biorfi 
 |-  ( ( ph /\ ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ F. ) ) )
4 df-ifp 
 |-  ( if- ( ph , ps , F. ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ F. ) ) )
5 3 4 bitr4i 
 |-  ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )