![]() |
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 130 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6bb 194 |
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 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: 3bitr4g 221 bibi2i 225 equsalh 1661 eueq3dc 2789 sbcel12g 2946 sbceqg 2947 sbcnel12g 2948 reldisj 3334 r19.3rm 3370 rabxp 4474 elrng 4627 iss 4758 eliniseg 4802 fcnvres 5194 dffv3g 5301 funimass4 5355 fndmdif 5404 fneqeql 5407 funimass3 5415 elrnrexdmb 5439 dff4im 5445 fconst4m 5517 elunirn 5545 riota1 5626 riota2df 5628 f1ocnvfv3 5641 eqfnov 5751 caoftrn 5880 mpt2xopovel 6006 rntpos 6022 ordgt0ge1 6199 iinerm 6362 erinxp 6364 qliftfun 6372 mapdm0 6418 isomnimap 6791 pr2nelem 6817 indpi 6899 genpdflem 7064 genpdisj 7080 genpassl 7081 genpassu 7082 ltnqpri 7151 ltpopr 7152 ltexprlemm 7157 ltexprlemdisj 7163 ltexprlemloc 7164 ltrennb 7389 letri3 7564 letr 7566 ltneg 7938 leneg 7941 reapltxor 8064 apsym 8081 suprnubex 8412 suprleubex 8413 elnnnn0 8714 zrevaddcl 8798 znnsub 8799 znn0sub 8813 prime 8843 eluz2 9023 eluz2b1 9086 nn01to3 9100 qrevaddcl 9127 xrletri3 9268 xrletr 9271 iccid 9341 elicopnf 9385 fzsplit2 9462 fzsn 9477 fzpr 9487 uzsplit 9502 fvinim0ffz 9648 lt2sqi 10038 le2sqi 10039 abs00ap 10491 mertenslem2 10926 gcddiv 11282 algcvgblem 11305 isprm3 11374 bj-sseq 11647 nnti 11847 |
Copyright terms: Public domain | W3C validator |