MPE Home 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- ( ph ,  ps ,  ch ) is "if  ph then  ps, and if not  ph then  ch." 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- (
ph ,  ps ,  ch )  <->  ( ( ph  ->  ps )  /\  ( -.  ph  ->  ch )
) )

Proof of Theorem dfifp2
StepHypRef Expression
1 df-ifp 1421 . 2  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
2 cases2 980 . 2  |-  ( ( ( ph  /\  ps )  \/  ( -.  ph 
/\  ch ) )  <->  ( ( ph  ->  ps )  /\  ( -.  ph  ->  ch ) ) )
31, 2bitri 252 1  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  ->  ps )  /\  ( -.  ph  ->  ch )
) )
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