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

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

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1059 . 2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 cases2 1043 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
31, 2bitri 278 1 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  if-wif 1058
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 845  df-ifp 1059
This theorem is referenced by:  dfifp3  1061  dfifp5  1063  ifpdfbi  1066  ifpnOLD  1070  ifpimpda  1078  revwlk  32484  ifpbi2  40173  ifpbi3  40174  ifpbi23  40179  ifpbi1  40183  ifpbi12  40194  ifpbi13  40195  ifpimimb  40210  ifpororb  40211  ifpbibib  40216  frege54cor0a  40562
  Copyright terms: Public domain W3C validator