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 2910 rmob 3047 preqr1g 3753 issod 4304 sotritrieq 4310 nsuceq0g 4403 suctr 4406 nordeq 4528 suc11g 4541 iss 4937 poirr2 5003 xp11m 5049 tz6.12c 5526 fnbrfvb 5537 fvelimab 5552 foeqcnvco 5769 f1eqcocnv 5770 acexmidlemcase 5848 nna0r 6457 nnawordex 6508 ectocld 6579 ecoptocl 6600 mapsn 6668 eqeng 6744 fopwdom 6814 ordiso 7013 ltexnqq 7370 nsmallnqq 7374 nqprloc 7507 aptiprleml 7601 map2psrprg 7767 0re 7920 lttri3 7999 0cnALT 8109 reapti 8498 recnz 9305 zneo 9313 uzn0 9502 flqidz 10242 ceilqidz 10272 modqid2 10307 modqmuladdnn0 10324 frec2uzrand 10361 frecuzrdgtcl 10368 seq3id 10464 seq3z 10467 facdiv 10672 facwordi 10674 maxleb 11180 fsumf1o 11353 dvdsnegb 11770 odd2np1lem 11831 odd2np1 11832 ltoddhalfle 11852 halfleoddlt 11853 opoe 11854 omoe 11855 opeo 11856 omeo 11857 gcddiv 11974 gcdzeq 11977 dvdssqim 11979 lcmgcdeq 12037 coprmdvds2 12047 rpmul 12052 divgcdcoprmex 12056 cncongr2 12058 dvdsprm 12091 coprm 12098 prmdvdsexp 12102 prmdiv 12189 pythagtriplem19 12236 pc2dvds 12283 pcadd 12293 prmpwdvds 12307 exmidunben 12381 intopsn 12621 ismgmid 12631 isgrpid2 12743 isgrpinv 12756 baspartn 12842 bastop 12869 isopn3 12919 lgsdir 13730 lgsne0 13733 bj-peano4 13990 sbthomlem 14057 |
Copyright terms: Public domain | W3C validator |