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

Theorem meetle 15785
 Description: A meet is less than or equal to a third value iff each argument is less than or equal to the third value. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
Hypotheses
Ref Expression
meetle.b
meetle.l
meetle.m
meetle.k
meetle.x
meetle.y
meetle.z
meetle.e
Assertion
Ref Expression
meetle

Proof of Theorem meetle
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 meetle.z . . 3
2 meetle.b . . . . 5
3 meetle.l . . . . 5
4 meetle.m . . . . 5
5 meetle.k . . . . 5
6 meetle.x . . . . 5
7 meetle.y . . . . 5
8 meetle.e . . . . 5
92, 3, 4, 5, 6, 7, 8meetlem 15782 . . . 4
109simprd 463 . . 3
11 breq1 4459 . . . . . 6
12 breq1 4459 . . . . . 6
1311, 12anbi12d 710 . . . . 5
14 breq1 4459 . . . . 5
1513, 14imbi12d 320 . . . 4
1615rspcva 3208 . . 3
171, 10, 16syl2anc 661 . 2
182, 3, 4, 5, 6, 7, 8lemeet1 15783 . . . 4
192, 4, 5, 6, 7, 8meetcl 15777 . . . . 5
202, 3postr 15710 . . . . 5
215, 1, 19, 6, 20syl13anc 1230 . . . 4
2218, 21mpan2d 674 . . 3
232, 3, 4, 5, 6, 7, 8lemeet2 15784 . . . 4
242, 3postr 15710 . . . . 5
255, 1, 19, 7, 24syl13anc 1230 . . . 4
2623, 25mpan2d 674 . . 3