Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  paddasslem10 Structured version   Unicode version

 Description: Lemma for paddass 30562. Use paddasslem4 30547 to eliminate from paddasslem9 30552. (Contributed by NM, 9-Jan-2012.)
Hypotheses
Ref Expression
Assertion
Ref Expression

Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl11 1032 . . . 4
2 simpl3l 1012 . . . 4
3 simpl3r 1013 . . . 4
41, 2, 33jca 1134 . . 3
5 an6 1263 . . . . . 6
6 ssel2 3335 . . . . . . 7
7 ssel2 3335 . . . . . . 7
8 ssel2 3335 . . . . . . 7
96, 7, 83anim123i 1139 . . . . . 6
105, 9sylbi 188 . . . . 5
11103ad2antl2 1120 . . . 4
13 simpl12 1033 . . . 4
14 simpl13 1034 . . . 4
15 simprr1 1005 . . . 4
1613, 14, 153jca 1134 . . 3
17 simprr2 1006 . . 3
18 simprr3 1007 . . 3
19 paddasslem.l . . . 4
20 paddasslem.j . . . 4
21 paddasslem.a . . . 4
2219, 20, 21paddasslem4 30547 . . 3
234, 12, 16, 17, 18, 22syl32anc 1192 . 2
24 simpl2 961 . . . . 5
25 simpl3 962 . . . . 5
261, 24, 253jca 1134 . . . 4