![]() |
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 1194 19.30dc 1515 nf4r 1558 cbvexh 1635 equveli 1639 sbequilem 1716 sb5rf 1729 nfsbxy 1815 nfsbxyt 1816 sbcomxyyz 1843 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 mo2n 1925 mo23 1938 2exeu 1989 bm1.1 2022 necon1idc 2252 sbhypf 2597 vtocl2 2603 vtocl3 2604 reu6 2724 rmo2ilem 2841 uneqin 3182 abn0r 3237 inelcm 3276 vdif0im 3281 difrab0eqim 3282 r19.3rm 3304 r19.9rmv 3307 difprsn1 3494 intminss 3631 bm1.3ii 3869 intexabim 3897 copsex2g 3974 opelopabt 3990 eusv2nf 4154 reusv3i 4157 ordtri2orexmid 4211 setindel 4221 tfi 4248 mosubopt 4348 eqrelrel 4384 xpiindim 4416 opeliunxp2 4419 opelrn 4511 issref 4650 xpmlem 4687 rnxpid 4698 ssxpbm 4699 relcoi2 4791 unixpm 4796 cnviinm 4802 iotanul 4825 funimaexglem 4925 fvelrnb 5164 fvmptssdm 5198 fnfvrnss 5268 fressnfv 5293 fconstfvm 5322 f1mpt 5353 ovprc 5482 fo1stresm 5730 fo2ndresm 5731 reldmtpos 5809 tfrlem5 5871 tfrlem9 5876 tfri2 5893 ener 6195 domtr 6201 unen 6229 distrnqg 6371 nqnq0pi 6421 nqnq0a 6437 nqnq0m 6438 distrnq0 6442 nqprloc 6528 ltexprlemopl 6575 ltexprlemopu 6577 recexre 7362 nn1suc 7714 msqznn 8114 nn0ind 8128 fnn0ind 8130 ublbneg 8324 qreccl 8351 fzo1fzo0n0 8809 elfzom1elp1fzo 8828 fzo0end 8849 fzind2 8865 redivap 9102 imdivap 9109 sqrt0 9213 bdbm1.3ii 9346 |
Copyright terms: Public domain | W3C validator |