Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dfifp2 | Structured version Visualization version GIF version |
Description: Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒". This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1064). (Contributed by BJ, 22-Jun-2019.) |
Ref | Expression |
---|---|
dfifp2 | ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ifp 1064 | . 2 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) | |
2 | cases2 1048 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | |
3 | 1, 2 | bitri 278 | 1 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 847 if-wif 1063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-ifp 1064 |
This theorem is referenced by: dfifp3 1066 dfifp5 1068 ifpdfbi 1071 ifpnOLD 1075 ifpimpda 1083 revwlk 32753 ifpbi2 40700 ifpbi3 40701 ifpbi23 40706 ifpbi1 40710 ifpbi12 40721 ifpbi13 40722 ifpimimb 40737 ifpororb 40738 ifpbibib 40743 frege54cor0a 41089 |
Copyright terms: Public domain | W3C validator |