Definition df-i0 43

Description: Define classical conditional.

Assertion

Ref	Expression
df-i0	(a ->0 b) = (a' v b)

Detailed syntax breakdown of Definition df-i0

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wi0 11	. 2 term (a ->0 b)
4	1	wn 4	. . 3 term a'
5	4, 2	wo 6	. 2 term (a' v b)
6	3, 5	wb 1	1 wff (a ->0 b) = (a' v b)

This definition is referenced by:  nom10 307  nom40 325  i0cmtrcom 495  u12lem 771  3vded21 817  3vded22 818  3vded3 819  3vroa 831  negant0 857  distoa 944  d3oa 995  oadist2a 1007  oacom 1011  oacom3 1013  oagen1 1014  oagen2 1016  oadistd 1023  lem3.3.2 1045  lem3.3.3 1051  lem3.3.7i0e1 1056  lem3.4.1 1074  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i1j0 1089  lem4.6.6i1j3 1091  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j0 1097  lem4.6.6i4j2 1098

Copyright terms: Public domain