![]() |
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 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6bb 185 |
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: 3bitr4g 212 bibi2i 216 equsalh 1614 eueq3dc 2715 sbcel12g 2865 sbceqg 2866 sbcnel12g 2867 reldisj 3271 r19.3rm 3310 rabxp 4380 elrng 4526 iss 4654 eliniseg 4695 fcnvres 5073 dffv3g 5174 funimass4 5224 fndmdif 5272 fneqeql 5275 funimass3 5283 elrnrexdmb 5307 dff4im 5313 fconst4m 5381 elunirn 5405 riota1 5486 riota2df 5488 f1ocnvfv3 5501 eqfnov 5607 caoftrn 5736 mpt2xopovel 5856 rntpos 5872 ordgt0ge1 6018 iinerm 6178 erinxp 6180 qliftfun 6188 indpi 6440 genpdflem 6605 genpdisj 6621 genpassl 6622 genpassu 6623 ltnqpri 6692 ltpopr 6693 ltexprlemm 6698 ltexprlemdisj 6704 ltexprlemloc 6705 ltrennb 6930 letri3 7099 letr 7101 ltneg 7457 leneg 7460 reapltxor 7580 apsym 7597 elnnnn0 8225 zrevaddcl 8295 znnsub 8296 znn0sub 8309 prime 8337 eluz2 8479 eluz2b1 8539 nn01to3 8552 qrevaddcl 8578 xrletri3 8721 xrletr 8724 iccid 8794 elicopnf 8838 fzsplit2 8914 fzsn 8929 fzpr 8939 uzsplit 8954 fvinim0ffz 9096 lt2sqi 9341 le2sqi 9342 abs00ap 9660 algcvgblem 9888 bj-sseq 9931 |
Copyright terms: Public domain | W3C validator |