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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimpcd 158 mob2 2892 rmob 3029 preqr1g 3731 issod 4281 sotritrieq 4287 nsuceq0g 4380 suctr 4383 nordeq 4505 suc11g 4518 iss 4914 poirr2 4980 xp11m 5026 tz6.12c 5500 fnbrfvb 5511 fvelimab 5526 foeqcnvco 5742 f1eqcocnv 5743 acexmidlemcase 5821 nna0r 6427 nnawordex 6477 ectocld 6548 ecoptocl 6569 mapsn 6637 eqeng 6713 fopwdom 6783 ordiso 6982 ltexnqq 7330 nsmallnqq 7334 nqprloc 7467 aptiprleml 7561 map2psrprg 7727 0re 7880 lttri3 7959 0cnALT 8069 reapti 8458 recnz 9262 zneo 9270 uzn0 9459 flqidz 10194 ceilqidz 10224 modqid2 10259 modqmuladdnn0 10276 frec2uzrand 10313 frecuzrdgtcl 10320 seq3id 10416 seq3z 10419 facdiv 10623 facwordi 10625 maxleb 11127 fsumf1o 11298 dvdsnegb 11715 odd2np1lem 11775 odd2np1 11776 ltoddhalfle 11796 halfleoddlt 11797 opoe 11798 omoe 11799 opeo 11800 omeo 11801 gcddiv 11918 gcdzeq 11921 dvdssqim 11923 lcmgcdeq 11975 coprmdvds2 11985 rpmul 11990 divgcdcoprmex 11994 cncongr2 11996 dvdsprm 12029 coprm 12034 prmdvdsexp 12038 prmdiv 12125 pythagtriplem19 12172 exmidunben 12225 baspartn 12518 bastop 12545 isopn3 12595 bj-peano4 13601 sbthomlem 13667 |
Copyright terms: Public domain | W3C validator |