MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfifp2 Structured version   Visualization version   GIF version

Theorem dfifp2 1007
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 1006). (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
dfifp2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1006 . 2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 cases2 1004 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
31, 2bitri 262 1 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  if-wif 1005
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 195  df-or 383  df-an 384  df-ifp 1006
This theorem is referenced by:  dfifp3  1008  dfifp5  1010  ifpn  1015  ifpimpda  1021  ifpbi2  36629  ifpbi3  36630  ifpbi23  36635  ifpbi1  36640  ifpbi12  36651  ifpbi13  36652  ifpbi123  36653  ifpimimb  36667  ifpororb  36668  ifpbibib  36673  frege54cor0a  36976
  Copyright terms: Public domain W3C validator