Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl12anc | Unicode version |
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Ref | Expression |
---|---|
sylXanc.1 | |
sylXanc.2 | |
sylXanc.3 | |
syl12anc.4 |
Ref | Expression |
---|---|
syl12anc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 | |
2 | sylXanc.2 | . . 3 | |
3 | sylXanc.3 | . . 3 | |
4 | 1, 2, 3 | jca32 293 | . 2 |
5 | syl12anc.4 | . 2 | |
6 | 4, 5 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: syl22anc 1136 cocan1 5427 fliftfun 5436 isopolem 5461 f1oiso2 5466 caovcld 5654 caovcomd 5657 tfrlemisucaccv 5939 fidceq 6330 findcard2d 6348 diffifi 6351 ordiso2 6357 prarloclemup 6593 prarloc 6601 nqprl 6649 nqpru 6650 ltaddpr 6695 aptiprlemu 6738 archpr 6741 cauappcvgprlem2 6758 caucvgprlem2 6778 caucvgprprlem2 6808 recexgt0sr 6858 archsr 6866 conjmulap 7705 lerec2 7855 ledivp1 7869 cju 7913 nn2ge 7946 gtndiv 8335 z2ge 8739 iccssioo2 8815 fzrev3 8949 elfz1b 8952 qbtwnzlemstep 9103 qbtwnzlemex 9105 rebtwn2zlemstep 9107 rebtwn2z 9109 qbtwnre 9111 flqdiv 9163 iseqcaopr 9242 expnegzap 9289 caucvgrelemrec 9578 resqrexlemex 9623 |
Copyright terms: Public domain | W3C validator |