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

Theorem dfifp2 1057
Description: Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒". This version of the definition uses only primitive symbols (→ , ¬ , ∀). This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1056). (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
dfifp2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1056 . 2 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 cases2 1040 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
31, 2bitri 276 1 (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  if-wif 1055
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 208  df-an 397  df-or 843  df-ifp 1056
This theorem is referenced by:  dfifp3  1058  dfifp5  1060  ifpn  1065  ifpimpda  1071  revwlk  31987  ifpbi2  39342  ifpbi3  39343  ifpbi23  39348  ifpbi1  39353  ifpbi12  39364  ifpbi13  39365  ifpimimb  39380  ifpororb  39381  ifpbibib  39386  frege54cor0a  39719
  Copyright terms: Public domain W3C validator