![]() |
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 132 | . 2 ⊢ (𝜒 ↔ 𝜓) |
4 | 1, 3 | bitr2di 197 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
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 4202 unisucg 4413 relsng 4728 funssres 5257 fncnv 5281 dff1o5 5469 funimass4 5565 fneqeql2 5624 fnniniseg2 5638 rexsupp 5639 unpreima 5640 dffo3 5662 funfvima 5746 dff13 5766 f1eqcocnv 5789 fliftf 5797 isocnv2 5810 eloprabga 5959 mpo2eqb 5981 opabex3d 6119 opabex3 6120 elxp6 6167 elxp7 6168 sbthlemi5 6957 sbthlemi6 6958 nninfwlporlemd 7167 genpdflem 7503 ltnqpr 7589 ltexprlemloc 7603 xrlenlt 8018 negcon2 8206 dfinfre 8909 sup3exmid 8910 elznn 9265 zq 9622 rpnegap 9682 modqmuladdnn0 10363 shftdm 10824 rexfiuz 10991 rexanuz2 10993 sumsplitdc 11433 fsum2dlemstep 11435 odd2np1 11870 divalgb 11922 infssuzex 11942 isprm4 12111 ctiunctlemudc 12430 grp1 12908 nmznsg 13004 iscrng2 13129 tx1cn 13640 tx2cn 13641 cnbl0 13905 cnblcld 13906 reopnap 13909 pilem1 14071 sinq34lt0t 14123 |
Copyright terms: Public domain | W3C validator |