![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr4id | GIF 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 131 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 1, 3 | bitr2di 196 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imimorbdc 882 baib 905 pm5.6dc 912 xornbidc 1370 mo2dc 2058 reu8 2904 sbc6g 2957 dfss4st 3336 r19.28m 3479 r19.45mv 3483 r19.44mv 3484 r19.27m 3485 ralsnsg 3592 ralsns 3593 iunconstm 3853 iinconstm 3854 exmidsssnc 4159 unisucg 4369 relsng 4682 funssres 5205 fncnv 5229 dff1o5 5416 funimass4 5512 fneqeql2 5569 fnniniseg2 5583 rexsupp 5584 unpreima 5585 dffo3 5607 funfvima 5689 dff13 5709 f1eqcocnv 5732 fliftf 5740 isocnv2 5753 eloprabga 5898 mpo2eqb 5920 opabex3d 6059 opabex3 6060 elxp6 6107 elxp7 6108 sbthlemi5 6894 sbthlemi6 6895 genpdflem 7406 ltnqpr 7492 ltexprlemloc 7506 xrlenlt 7921 negcon2 8107 dfinfre 8806 sup3exmid 8807 elznn 9162 zq 9513 rpnegap 9571 modqmuladdnn0 10245 shftdm 10699 rexfiuz 10866 rexanuz2 10868 sumsplitdc 11306 fsum2dlemstep 11308 odd2np1 11737 divalgb 11789 infssuzex 11809 isprm4 11967 ctiunctlemudc 12117 tx1cn 12608 tx2cn 12609 cnbl0 12873 cnblcld 12874 reopnap 12877 pilem1 13039 sinq34lt0t 13091 |
Copyright terms: Public domain | W3C validator |