Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl3an1 | Unicode version |
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
Ref | Expression |
---|---|
syl3an1.1 | |
syl3an1.2 |
Ref | Expression |
---|---|
syl3an1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3an1.1 | . . 3 | |
2 | 1 | 3anim1i 1180 | . 2 |
3 | syl3an1.2 | . 2 | |
4 | 2, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: syl3an1b 1269 syl3an1br 1272 wepo 4344 f1ofveu 5841 fovrnda 5996 smoiso 6281 tfrcl 6343 omv 6434 oeiv 6435 nndi 6465 nnmsucr 6467 f1oen2g 6733 f1dom2g 6734 undiffi 6902 prarloclemarch2 7381 distrnq0 7421 ltprordil 7551 1idprl 7552 1idpru 7553 ltpopr 7557 ltexprlemopu 7565 ltexprlemdisj 7568 ltexprlemfl 7571 ltexprlemfu 7573 ltexprlemru 7574 recexprlemdisj 7592 recexprlemss1l 7597 recexprlemss1u 7598 cnegexlem1 8094 msqge0 8535 mulge0 8538 divnegap 8623 divdiv32ap 8637 divneg2ap 8653 peano2uz 9542 lbzbi 9575 negqmod0 10287 modqmuladdnn0 10324 expnlbnd 10600 shftfvalg 10782 xrmaxaddlem 11223 retanclap 11685 tannegap 11691 demoivreALT 11736 gcd0id 11934 isprm3 12072 euclemma 12100 phiprmpw 12176 fermltl 12188 mndcl 12659 grpcl 12716 dfgrp2 12732 grprcan 12740 psmetcl 13120 xmetcl 13146 metcl 13147 meteq0 13154 metge0 13160 metsym 13165 blelrnps 13213 blelrn 13214 blssm 13215 blres 13228 mscl 13259 xmscl 13260 xmsge0 13261 xmseq0 13262 xmssym 13263 mopnin 13281 sincosq1sgn 13541 sincosq2sgn 13542 sincosq3sgn 13543 sincosq4sgn 13544 lgsneg1 13720 |
Copyright terms: Public domain | W3C validator |