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 1152 | . 2 |
3 | syl3an1.2 | . 2 | |
4 | 2, 3 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 947 |
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 949 |
This theorem is referenced by: syl3an1b 1237 syl3an1br 1240 wepo 4251 f1ofveu 5730 fovrnda 5882 smoiso 6167 tfrcl 6229 omv 6319 oeiv 6320 nndi 6350 nnmsucr 6352 f1oen2g 6617 f1dom2g 6618 undiffi 6781 prarloclemarch2 7195 distrnq0 7235 ltprordil 7365 1idprl 7366 1idpru 7367 ltpopr 7371 ltexprlemopu 7379 ltexprlemdisj 7382 ltexprlemfl 7385 ltexprlemfu 7387 ltexprlemru 7388 recexprlemdisj 7406 recexprlemss1l 7411 recexprlemss1u 7412 cnegexlem1 7905 msqge0 8346 mulge0 8349 divnegap 8434 divdiv32ap 8448 divneg2ap 8464 peano2uz 9346 lbzbi 9376 negqmod0 10072 modqmuladdnn0 10109 expnlbnd 10384 shftfvalg 10558 xrmaxaddlem 10997 retanclap 11356 tannegap 11362 demoivreALT 11407 gcd0id 11594 isprm3 11726 euclemma 11751 phiprmpw 11825 psmetcl 12422 xmetcl 12448 metcl 12449 meteq0 12456 metge0 12462 metsym 12467 blelrnps 12515 blelrn 12516 blssm 12517 blres 12530 mscl 12561 xmscl 12562 xmsge0 12563 xmseq0 12564 xmssym 12565 mopnin 12583 sincosq1sgn 12834 sincosq2sgn 12835 sincosq3sgn 12836 sincosq4sgn 12837 |
Copyright terms: Public domain | W3C validator |