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

Definition df-ifp 1389
Description: Definition of the conditional operator for propositions. The value of if- ( ph ,  ps ,  ch ) is  ps if  ph is true and  ch if  ph false. See dfifp2 1390, dfifp3 1391, dfifp4 1392, dfifp5 1393, dfifp6 1394 and dfifp7 1395 for alternate definitions. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
df-ifp  |-  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )

Detailed syntax breakdown of Definition df-ifp
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3wif 1388 . 2  wff if- ( ph ,  ps ,  ch )
51, 2wa 369 . . 3  wff  ( ph  /\ 
ps )
61wn 3 . . . 4  wff  -.  ph
76, 3wa 369 . . 3  wff  ( -. 
ph  /\  ch )
85, 7wo 368 . 2  wff  ( (
ph  /\  ps )  \/  ( -.  ph  /\  ch ) )
94, 8wb 186 1  wff  (if- (
ph ,  ps ,  ch )  <->  ( ( ph  /\ 
ps )  \/  ( -.  ph  /\  ch )
) )
Colors of variables: wff setvar class
This definition is referenced by:  dfifp2  1390  dfifp6  1394  ifpor  1397  casesifp  1404  bj-df-ifc  30742  ifpdfan  35569  ifpnot23  35582
  Copyright terms: Public domain W3C validator