![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylbir | Unicode version |
Description: A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sylbir.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
sylbir.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylbir |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylbir.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpri 124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | sylbir.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 |
This theorem is referenced by: 3imtr3i 189 3ori 1195 19.30dc 1518 nf4r 1561 cbvexh 1638 equveli 1642 sbequilem 1719 sb5rf 1732 nfsbxy 1818 nfsbxyt 1819 sbcomxyyz 1846 dvelimALT 1886 dvelimfv 1887 dvelimor 1894 mo2n 1928 mo23 1941 2exeu 1992 bm1.1 2025 necon1idc 2258 sbhypf 2603 vtocl2 2609 vtocl3 2610 reu6 2730 rmo2ilem 2847 uneqin 3188 abn0r 3243 inelcm 3282 vdif0im 3287 difrab0eqim 3288 r19.3rm 3310 r19.9rmv 3313 difprsn1 3503 intminss 3640 bm1.3ii 3878 intexabim 3906 copsex2g 3983 opelopabt 3999 eusv2nf 4188 reusv3i 4191 onintrab2im 4244 ordtri2orexmid 4248 setindel 4263 onsucuni2 4288 ordtri2or2exmid 4296 zfregfr 4298 tfi 4305 mosubopt 4405 eqrelrel 4441 xpiindim 4473 opeliunxp2 4476 opelrn 4568 issref 4707 xpmlem 4744 rnxpid 4755 ssxpbm 4756 relcoi2 4848 unixpm 4853 cnviinm 4859 iotanul 4882 funimaexglem 4982 fvelrnb 5221 fvmptssdm 5255 fnfvrnss 5325 fressnfv 5350 fconstfvm 5379 f1mpt 5410 ovprc 5540 fo1stresm 5788 fo2ndresm 5789 reldmtpos 5868 tfrlem5 5930 tfrlem9 5935 tfri2 5952 ener 6259 domtr 6265 unen 6293 cardval3ex 6365 distrnqg 6485 nqnq0pi 6536 nqnq0a 6552 nqnq0m 6553 distrnq0 6557 nqprloc 6643 ltexprlemopl 6699 ltexprlemopu 6701 recexre 7569 nn1suc 7933 msqznn 8338 nn0ind 8352 fnn0ind 8354 ublbneg 8548 qreccl 8576 fzo1fzo0n0 9039 elfzom1elp1fzo 9058 fzo0end 9079 fzind2 9095 flqeqceilz 9160 iser0f 9251 redivap 9474 imdivap 9481 cvg1nlemres 9584 sqrt0 9602 ialgfx 9891 bdbm1.3ii 10011 |
Copyright terms: Public domain | W3C validator |