Definition df-i2 45

Description: Define Dishkant conditional.

Assertion

Ref	Expression
df-i2	(a ->2 b) = (b v (a' ^ b'))

Detailed syntax breakdown of Definition df-i2

Step	Hyp	Ref	Expression
1		wva	. . 3 term a
2		wvb	. . 3 term b
3	1, 2	wi2 13	. 2 term (a ->2 b)
4	1	wn 4	. . . 4 term a'
5	2	wn 4	. . . 4 term b'
6	4, 5	wa 7	. . 3 term (a' ^ b')
7	2, 6	wo 6	. 2 term (b v (a' ^ b'))
8	3, 7	wb 1	1 wff (a ->2 b) = (b v (a' ^ b'))

This definition is referenced by:  ud2lem0a 252  ud2lem0b 253  i1i2 260  i2id 270  ud2lem0c 272  wql2lem 282  wql2lem2 283  wql2lem3 284  wql2lem5 286  wql1 287  nom12 303  i2or 338  lei2 340  i5lei2 342  2vwomr1a 349  2vwomr2a 350  2vwomlem 351  wr5-2v 352  woml6 422  woml7 423  ud2lem1 549  ud2lem2 550  ud2lem3 551  u2lemaa 587  u2lemana 592  u2lemab 597  u2lemanb 602  u2lemoa 607  u2lemona 612  u2lemob 617  u2lemonb 622  u2lemc1 667  u2lemc2 673  u2lemc4 688  comi12 693  u2lemle2 702  u2lembi 707  i2bi 708  u12lembi 712  u2lem1 721  u2lem2 731  u2lem3 736  u2lem5 748  u24lem 756  u12lem 757  u2lem7 759  u2lem8 768  i2i1i1 786  3vth1 790  3vth4 793  3vth5 794  3vth6 795  3vth7 796  3vth9 798  3vded21 803  3vded22 804  1oa 806  1oaii 810  2oalem1 811  2oath1 812  oale 815  3vroa 817  salem1 823  bi3 825  orbi 828  negant2 844  mlaconjolem 871  govar 882  govar2 883  oa4lem1 923  oa4lem2 924  distoah4 929  d3oa 981  oalii 988  oaliv 989  oalem1 991  oadist2a 993  mloa 1004  lem3.3.4 1038  lem3.3.6 1041  lem3.3.7i2e1 1048  lem4.6.6i0j2 1072  lem4.6.6i2j0 1078  lem4.6.6i2j1 1079  lem4.6.6i2j4 1080  lem4.6.6i4j2 1084  wdwom 1089

Copyright terms: Public domain