![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5bb | GIF version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5bb.1 | ⊢ (𝜑 ↔ 𝜓) |
syl5bb.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5bb | ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5bb.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
3 | syl5bb.2 | . 2 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
4 | 2, 3 | bitrd 177 | 1 ⊢ (𝜒 → (𝜑 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: syl5rbb 182 syl5bbr 183 3bitr4g 212 imim21b 241 pm5.17dc 810 dn1dc 867 bilukdc 1287 nf4dc 1560 sbal1 1878 abbi 2151 necon3abid 2244 necon3bid 2246 necon1abiidc 2265 r19.21t 2394 ceqsralt 2581 ceqsrexv 2674 ceqsrex2v 2676 elab2g 2689 elrabf 2696 eueq2dc 2714 euxfrdc 2727 eqreu 2733 reu8 2737 ru 2763 sbcralt 2834 sbcrext 2835 sbcne12g 2868 csbnestgf 2898 disjpss 3278 ralprg 3421 rexprg 3422 difsn 3501 opthpr 3543 ralunsn 3568 dfiin2g 3690 iunxsng 3732 elpwuni 3741 pwnss 3912 opelopabt 3999 opelopabga 4000 brabga 4001 elsucg 4141 elsuc2g 4142 brab2a 4393 opeliunxp 4395 posng 4412 brab2ga 4415 csbdmg 4529 elrnmpt1 4585 elrnmptg 4586 poleloe 4724 elxp4 4808 elxp5 4809 cnvpom 4860 sbcfung 4925 dffun8 4929 fncnv 4965 fununi 4967 fnssresb 5011 fnimaeq0 5020 funcocnv2 5151 dffn5im 5219 funimass4 5224 fnsnfv 5232 dmfco 5241 fndmdif 5272 fndmin 5274 unpreima 5292 respreima 5295 fsn2 5337 fnressn 5349 fressnfv 5350 elunirn 5405 dff13 5407 fliftel 5433 isoini 5457 f1oiso 5465 acexmid 5511 eloprabga 5591 resoprab2 5598 ralrnmpt2 5615 rexrnmpt2 5616 ovid 5617 ov 5620 ovg 5639 ofrfval2 5727 fmpt2x 5826 1stconst 5842 2ndconst 5843 isprmpt2 5858 brtpos2 5866 dfsmo2 5902 brdifun 6133 eqerlem 6137 brecop 6196 erovlem 6198 xpsnen 6295 xpdom2 6305 ltpiord 6417 nlt1pig 6439 elinp 6572 ltdfpr 6604 genpassl 6622 genpassu 6623 1idprl 6688 1idpru 6689 gt0srpr 6833 peano2nnnn 6929 recidpirq 6934 axprecex 6954 xrlenlt 7084 addsubeq4 7226 renegcl 7272 lesub0 7474 recexaplem2 7633 conjmulap 7705 rerecclap 7706 creui 7912 peano2nn 7926 nndiv 7954 elznn0 8260 eqreznegel 8549 ltxr 8695 divelunit 8870 iccf1o 8872 elfz2 8881 elfzp1 8934 fzdifsuc 8943 fznn 8951 fzosplitsni 9091 fvinim0ffz 9096 frec2uzisod 9193 sq11i 9343 cjreb 9466 cau3lem 9710 bj-indeq 10053 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |