Theorem 3vded12 815

Description: A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)

Hypotheses

Ref	Expression
3vded12.1	(a ∩ (c →1 a)) ≤ (c →1 (b →1 a))
3vded12.2	c ≤ a

Assertion

Ref	Expression
3vded12	c ≤ (b →1 a)

Proof of Theorem 3vded12

Step	Hyp	Ref	Expression
1		le1 146	. . 3 (c →1 (b →1 a)) ≤ 1
2		df-t 41	. . . 4 1 = (a ∪ a⊥ )
3		an1 106	. . . . . . . 8 (a ∩ 1) = a
4	3	ax-r1 35	. . . . . . 7 a = (a ∩ 1)
5		3vded12.2	. . . . . . . . . 10 c ≤ a
6	5	u1lemle1 710	. . . . . . . . 9 (c →1 a) = 1
7	6	lan 77	. . . . . . . 8 (a ∩ (c →1 a)) = (a ∩ 1)
8	7	ax-r1 35	. . . . . . 7 (a ∩ 1) = (a ∩ (c →1 a))
9	4, 8	ax-r2 36	. . . . . 6 a = (a ∩ (c →1 a))
10		3vded12.1	. . . . . 6 (a ∩ (c →1 a)) ≤ (c →1 (b →1 a))
11	9, 10	bltr 138	. . . . 5 a ≤ (c →1 (b →1 a))
12	5	lecon 154	. . . . . 6 a⊥ ≤ c⊥
13		leo 158	. . . . . . 7 c⊥ ≤ (c⊥ ∪ (c ∩ (b →1 a)))
14		df-i1 44	. . . . . . . 8 (c →1 (b →1 a)) = (c⊥ ∪ (c ∩ (b →1 a)))
15	14	ax-r1 35	. . . . . . 7 (c⊥ ∪ (c ∩ (b →1 a))) = (c →1 (b →1 a))
16	13, 15	lbtr 139	. . . . . 6 c⊥ ≤ (c →1 (b →1 a))
17	12, 16	letr 137	. . . . 5 a⊥ ≤ (c →1 (b →1 a))
18	11, 17	lel2or 170	. . . 4 (a ∪ a⊥ ) ≤ (c →1 (b →1 a))
19	2, 18	bltr 138	. . 3 1 ≤ (c →1 (b →1 a))
20	1, 19	lebi 145	. 2 (c →1 (b →1 a)) = 1
21	20	u1lemle2 715	1 c ≤ (b →1 a)

Syntax hints:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by: (None)