Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syld3an3 | Unicode version |
Description: A syllogism inference. (Contributed by NM, 20-May-2007.) |
Ref | Expression |
---|---|
syld3an3.1 | |
syld3an3.2 |
Ref | Expression |
---|---|
syld3an3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 904 | . 2 | |
2 | simp2 905 | . 2 | |
3 | syld3an3.1 | . 2 | |
4 | syld3an3.2 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1135 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: syld3an1 1181 syld3an2 1182 brelrng 4565 moriotass 5496 nnncan1 7247 lediv1 7835 modqval 9166 modqvalr 9167 modqcl 9168 flqpmodeq 9169 modq0 9171 modqge0 9174 modqlt 9175 modqdiffl 9177 modqdifz 9178 expival 9257 |
Copyright terms: Public domain | W3C validator |