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

Theorem dfifp2 1422
 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 1421). (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
dfifp2 if-

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1421 . 2 if-
2 cases2 980 . 2
31, 2bitri 252 1 if-
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wo 369   wa 370  if-wif 1420 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 188  df-or 371  df-an 372  df-ifp 1421 This theorem is referenced by:  dfifp3  1423  dfifp5  1425  ifpn  1430  ifpbi2  36017  ifpbi3  36018  ifpbi23  36023  ifpbi1  36028  ifpbi12  36039  ifpbi13  36040  ifpbi123  36041  ifpimimb  36055  ifpororb  36056  ifpbibib  36061  frege54cor0a  36366
 Copyright terms: Public domain W3C validator