![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5ibcom | GIF version |
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.) |
Ref | Expression |
---|---|
imbitrid.1 | ⊢ (𝜑 → 𝜓) |
imbitrid.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5ibcom | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbitrid.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | imbitrid.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | imbitrid 154 | . 2 ⊢ (𝜒 → (𝜑 → 𝜃)) |
4 | 3 | com12 30 | 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 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biimpcd 159 mob2 2919 rmob 3057 preqr1g 3768 issod 4321 sotritrieq 4327 nsuceq0g 4420 suctr 4423 nordeq 4545 suc11g 4558 iss 4955 poirr2 5023 xp11m 5069 tz6.12c 5547 fnbrfvb 5559 fvelimab 5575 foeqcnvco 5794 f1eqcocnv 5795 acexmidlemcase 5873 nna0r 6482 nnawordex 6533 ectocld 6604 ecoptocl 6625 mapsn 6693 eqeng 6769 fopwdom 6839 ordiso 7038 ltexnqq 7410 nsmallnqq 7414 nqprloc 7547 aptiprleml 7641 map2psrprg 7807 0re 7960 lttri3 8040 0cnALT 8150 reapti 8539 recnz 9349 zneo 9357 uzn0 9546 flqidz 10289 ceilqidz 10319 modqid2 10354 modqmuladdnn0 10371 frec2uzrand 10408 frecuzrdgtcl 10415 seq3id 10511 seq3z 10514 facdiv 10721 facwordi 10723 maxleb 11228 fsumf1o 11401 dvdsnegb 11818 odd2np1lem 11880 odd2np1 11881 ltoddhalfle 11901 halfleoddlt 11902 opoe 11903 omoe 11904 opeo 11905 omeo 11906 gcddiv 12023 gcdzeq 12026 dvdssqim 12028 lcmgcdeq 12086 coprmdvds2 12096 rpmul 12101 divgcdcoprmex 12105 cncongr2 12107 dvdsprm 12140 coprm 12147 prmdvdsexp 12151 prmdiv 12238 pythagtriplem19 12285 pc2dvds 12332 pcadd 12342 prmpwdvds 12356 exmidunben 12430 intopsn 12792 ismgmid 12802 isgrpid2 12919 isgrpinv 12932 dfgrp3mlem 12974 dvdsrcl2 13274 dvdsrtr 13276 dvdsrmul1 13277 lspsneq0 13518 dvdsrzring 13633 baspartn 13690 bastop 13715 isopn3 13765 lgsdir 14576 lgsne0 14579 bj-peano4 14847 sbthomlem 14914 |
Copyright terms: Public domain | W3C validator |