![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2and | Structured version Visualization version Unicode version |
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
Ref | Expression |
---|---|
syl2and.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl2and.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl2and.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl2and |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2and.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl2and.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | syl2and.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sylan2d 485 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | syland 484 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 189 df-an 373 |
This theorem is referenced by: anim12d 566 ax7 1860 dffi3 7945 cflim2 8693 axpre-sup 9593 xle2add 11545 fzen 11816 rpmulgcd2 14662 pcqmul 14803 initoeu1 15906 termoeu1 15913 plttr 16216 pospo 16219 lublecllem 16234 latjlej12 16313 latmlem12 16329 cygabl 17525 hausnei2 20369 uncmp 20418 itgsubst 23001 dvdsmulf1o 24123 2sqlem8a 24299 axcontlem9 25002 usg2wotspth 25612 numclwlk1lem2f1 25822 shintcli 26982 cvntr 27945 cdj3i 28094 bj-bary1 31717 heicant 31975 itg2addnc 31996 dihmeetlem1N 34858 |
Copyright terms: Public domain | W3C validator |