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

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

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1060 . 2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 cases2 1044 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
31, 2bitri 274 1 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 843  if-wif 1059
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 206  df-an 395  df-or 844  df-ifp 1060
This theorem is referenced by:  dfifp3  1062  dfifp5  1064  ifpdfbi  1067  ifpnOLD  1071  ifpimpda  1079  revwlk  34413  ifpbi2  42520  ifpbi3  42521  ifpbi1  42530  ifpbi12  42541  ifpbi13  42542  ifpimimb  42557  ifpororb  42558  ifpbibib  42563  frege54cor0a  42916
  Copyright terms: Public domain W3C validator