![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6bbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6bbr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6bbr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6bbr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bbr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6bbr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6bb 195 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3bitr4g 222 bibi2i 226 equsalh 1668 eueq3dc 2803 sbcel12g 2960 sbceqg 2961 sbcnel12g 2962 reldisj 3353 r19.3rm 3390 rabxp 4504 elrng 4658 iss 4791 eliniseg 4835 fcnvres 5229 dffv3g 5336 funimass4 5390 fndmdif 5443 fneqeql 5446 funimass3 5454 elrnrexdmb 5478 dff4im 5484 fconst4m 5556 elunirn 5583 riota1 5664 riota2df 5666 f1ocnvfv3 5679 eqfnov 5789 caoftrn 5918 mpt2xopovel 6044 rntpos 6060 ordgt0ge1 6237 iinerm 6404 erinxp 6406 qliftfun 6414 mapdm0 6460 isomnimap 6880 ismkvmap 6898 pr2nelem 6916 indpi 6998 genpdflem 7163 genpdisj 7179 genpassl 7180 genpassu 7181 ltnqpri 7250 ltpopr 7251 ltexprlemm 7256 ltexprlemdisj 7262 ltexprlemloc 7263 ltrennb 7488 letri3 7663 letr 7665 ltneg 8037 leneg 8040 reapltxor 8163 apsym 8180 suprnubex 8511 suprleubex 8512 elnnnn0 8814 zrevaddcl 8898 znnsub 8899 znn0sub 8913 prime 8944 eluz2 9124 eluz2b1 9187 nn01to3 9201 qrevaddcl 9228 xrletri3 9371 xrletr 9374 iccid 9491 elicopnf 9535 fzsplit2 9613 fzsn 9629 fzpr 9640 uzsplit 9655 fvinim0ffz 9801 lt2sqi 10157 le2sqi 10158 abs00ap 10610 iooinsup 10820 mertenslem2 11079 gcddiv 11435 algcvgblem 11458 isprm3 11527 eltg2b 11906 discld 11988 opnssneib 12008 restbasg 12020 ssidcn 12061 cnptoprest2 12091 lmss 12097 bldisj 12187 xmeter 12222 bl2ioo 12316 bj-sseq 12400 nnti 12597 |
Copyright terms: Public domain | W3C validator |