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

Definition df-ifp 1381
Description: Definition of the conditional operator for propositions. The value of is if is true and if false. See dfifp2 1382, dfifp3 1383, dfifp4 1384, dfifp5 1385, dfifp6 1386 and dfifp7 1387 for alternate definitions. (Contributed by BJ, 22-Jun-2019.)
Assertion
Ref Expression
df-ifp

Detailed syntax breakdown of Definition df-ifp
StepHypRef Expression
1 wph . . 3
2 wps . . 3
3 wch . . 3
41, 2, 3wif 1380 . 2
51, 2wa 369 . . 3
61wn 3 . . . 4
76, 3wa 369 . . 3
85, 7wo 368 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  dfifp2  1382  dfifp6  1386  casesifp  1392  ifpor  34159  bj-df-ifc  34165  bj-ifnot23  37718  bj-ifdfan  37727
  Copyright terms: Public domain W3C validator