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

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

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1007 . 2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 cases2 1005 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
31, 2bitri 263 1 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  if-wif 1006
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 196  df-or 384  df-an 385  df-ifp 1007
This theorem is referenced by:  dfifp3  1009  dfifp5  1011  ifpn  1016  ifpimpda  1022  ifpbi2  36830  ifpbi3  36831  ifpbi23  36836  ifpbi1  36841  ifpbi12  36852  ifpbi13  36853  ifpbi123  36854  ifpimimb  36868  ifpororb  36869  ifpbibib  36874  frege54cor0a  37177
  Copyright terms: Public domain W3C validator