![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4di | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr4di.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitr4di.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr4di |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4di.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bitr4di.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitrdi 196 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: 3bitr4g 223 bibi2i 227 equsalh 1726 eueq3dc 2911 sbcel12g 3072 sbceqg 3073 sbcnel12g 3074 reldisj 3474 r19.3rm 3511 eldifpr 3619 eldiftp 3638 rabxp 4662 elrng 4817 iss 4952 eliniseg 4997 fcnvres 5398 dffv3g 5510 funimass4 5565 fndmdif 5620 fneqeql 5623 funimass3 5631 elrnrexdmb 5655 dff4im 5661 fconst4m 5735 elunirn 5764 riota1 5846 riota2df 5848 f1ocnvfv3 5861 eqfnov 5978 caoftrn 6105 mpoxopovel 6239 rntpos 6255 ordgt0ge1 6433 iinerm 6604 erinxp 6606 qliftfun 6614 mapdm0 6660 elfi2 6968 fifo 6976 inl11 7061 ctssdccl 7107 isomnimap 7132 ismkvmap 7149 iswomnimap 7161 omniwomnimkv 7162 pr2nelem 7187 indpi 7338 genpdflem 7503 genpdisj 7519 genpassl 7520 genpassu 7521 ltnqpri 7590 ltpopr 7591 ltexprlemm 7596 ltexprlemdisj 7602 ltexprlemloc 7603 ltrennb 7850 letri3 8034 letr 8036 ltneg 8415 leneg 8418 reapltxor 8542 apsym 8559 suprnubex 8906 suprleubex 8907 elnnnn0 9215 zrevaddcl 9299 znnsub 9300 znn0sub 9314 prime 9348 eluz2 9530 eluz2b1 9597 nn01to3 9613 qrevaddcl 9640 xrletri3 9800 xrletr 9804 iccid 9921 elicopnf 9965 fzsplit2 10045 fzsn 10061 fzpr 10072 uzsplit 10087 fvinim0ffz 10236 lt2sqi 10602 le2sqi 10603 abs00ap 11064 iooinsup 11278 mertenslem2 11537 fprod2dlemstep 11623 gcddiv 12012 algcvgblem 12041 isprm3 12110 phisum 12232 issubg 12964 resgrpisgrp 12986 eqgval 13013 ring1 13167 crngunit 13211 eltg2b 13425 discld 13507 opnssneib 13527 restbasg 13539 ssidcn 13581 cnptoprest2 13611 lmss 13617 txrest 13647 txlm 13650 imasnopn 13670 bldisj 13772 xmeter 13807 bl2ioo 13913 limcdifap 14002 bj-sseq 14404 nnti 14604 pw1nct 14612 |
Copyright terms: Public domain | W3C validator |