Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sylanl2 | Structured version Visualization version Unicode version |
Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
Ref | Expression |
---|---|
sylanl2.1 | |
sylanl2.2 |
Ref | Expression |
---|---|
sylanl2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanl2.1 | . . 3 | |
2 | 1 | anim2i 593 | . 2 |
3 | sylanl2.2 | . 2 | |
4 | 2, 3 | sylan 488 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: mpanlr1 722 adantlrl 756 adantlrr 757 oesuclem 7605 oelim 7614 mulsub 10473 divsubdiv 10741 lcmneg 15316 vdwlem12 15696 dpjidcl 18457 mplbas2 19470 monmat2matmon 20629 bwth 21213 cnextfun 21868 elbl4 22368 metucn 22376 dvradcnv 24175 dchrisum0lem2a 25206 axcontlem4 25847 cnlnadjlem2 28927 chirredlem2 29250 mdsymlem5 29266 sibfof 30402 relowlssretop 33211 matunitlindflem1 33405 poimirlem29 33438 unichnidl 33830 dmncan2 33876 cvrexchlem 34705 jm2.26 37569 radcnvrat 38513 binomcxplemnotnn0 38555 suplesup 39555 dvnmptdivc 40153 fourierdlem64 40387 fourierdlem74 40397 fourierdlem75 40398 fourierdlem83 40406 etransclem35 40486 iundjiun 40677 hoidmvlelem2 40810 |
Copyright terms: Public domain | W3C validator |