![]() |
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 |
---|---|
syl5ib.1 | ⊢ (𝜑 → 𝜓) |
syl5ib.2 | ⊢ (𝜒 → (𝜓 ↔ 𝜃)) |
Ref | Expression |
---|---|
syl5ibcom | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5ib.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl5ib.2 | . . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃)) | |
3 | 1, 2 | syl5ib 153 | . 2 ⊢ (𝜒 → (𝜑 → 𝜃)) |
4 | 3 | com12 30 | 1 ⊢ (𝜑 → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpcd 158 mob2 2796 rmob 2932 preqr1g 3616 issod 4155 sotritrieq 4161 nsuceq0g 4254 suctr 4257 nordeq 4373 suc11g 4386 iss 4771 poirr2 4837 xp11m 4882 tz6.12c 5347 fnbrfvb 5358 fvelimab 5373 foeqcnvco 5583 f1eqcocnv 5584 acexmidlemcase 5661 nna0r 6253 nnawordex 6301 ectocld 6372 ecoptocl 6393 mapsn 6461 eqeng 6537 fopwdom 6606 ordiso 6783 ltexnqq 7021 nsmallnqq 7025 nqprloc 7158 aptiprleml 7252 0re 7542 lttri3 7619 0cnALT 7726 reapti 8110 recnz 8893 zneo 8901 uzn0 9088 flqidz 9747 ceilqidz 9777 modqid2 9812 modqmuladdnn0 9829 frec2uzrand 9866 frecuzrdgtcl 9873 iseqid 9993 iseqz 9997 facdiv 10200 facwordi 10202 maxleb 10703 fsumf1o 10836 dvdsnegb 11145 odd2np1lem 11204 odd2np1 11205 ltoddhalfle 11225 halfleoddlt 11226 opoe 11227 omoe 11228 opeo 11229 omeo 11230 gcddiv 11340 gcdzeq 11343 dvdssqim 11345 lcmgcdeq 11397 coprmdvds2 11407 rpmul 11412 divgcdcoprmex 11416 cncongr2 11418 dvdsprm 11450 coprm 11455 prmdvdsexp 11459 baspartn 11802 bastop 11829 isopn3 11879 bj-peano4 12116 |
Copyright terms: Public domain | W3C validator |