![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4id | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
bitr4id.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
bitr4id.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr4id |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr4id.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | bitr4id.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr2di 197 |
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: imimorbdc 896 baib 919 pm5.6dc 926 xornbidc 1391 mo2dc 2081 reu8 2933 sbc6g 2987 dfss4st 3368 r19.28m 3512 r19.45mv 3516 r19.44mv 3517 r19.27m 3518 ralsnsg 3629 ralsns 3630 iunconstm 3894 iinconstm 3895 exmidsssnc 4203 unisucg 4414 relsng 4729 funssres 5258 fncnv 5282 dff1o5 5470 funimass4 5566 fneqeql2 5625 fnniniseg2 5639 rexsupp 5640 unpreima 5641 dffo3 5663 funfvima 5748 dff13 5768 f1eqcocnv 5791 fliftf 5799 isocnv2 5812 eloprabga 5961 mpo2eqb 5983 opabex3d 6121 opabex3 6122 elxp6 6169 elxp7 6170 sbthlemi5 6959 sbthlemi6 6960 nninfwlporlemd 7169 genpdflem 7505 ltnqpr 7591 ltexprlemloc 7605 xrlenlt 8020 negcon2 8208 dfinfre 8911 sup3exmid 8912 elznn 9267 zq 9624 rpnegap 9684 modqmuladdnn0 10365 shftdm 10826 rexfiuz 10993 rexanuz2 10995 sumsplitdc 11435 fsum2dlemstep 11437 odd2np1 11872 divalgb 11924 infssuzex 11944 isprm4 12113 ctiunctlemudc 12432 grp1 12930 nmznsg 13026 iscrng2 13151 tx1cn 13662 tx2cn 13663 cnbl0 13927 cnblcld 13928 reopnap 13931 pilem1 14093 sinq34lt0t 14145 |
Copyright terms: Public domain | W3C validator |