![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl21anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
syl21anc.4 | ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl21anc | ⊢ (𝜑 → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | jca31 309 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
5 | syl21anc.4 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
6 | 4, 5 | syl 14 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: issod 4318 brcogw 4795 funprg 5265 funtpg 5266 fnunsn 5322 ftpg 5699 fsnunf 5715 isotr 5814 off 6092 caofrss 6104 tfr1onlembxssdm 6341 tfrcllembxssdm 6354 pmresg 6673 ac6sfi 6895 tridc 6896 fidcenumlemrks 6949 sbthlemi8 6960 casefun 7081 caseinj 7085 djufun 7100 djuinj 7102 mulclpi 7324 archnqq 7413 addlocprlemlt 7527 addlocprlemeq 7529 addlocprlemgt 7530 mullocprlem 7566 apreim 8556 subrecap 8792 ltrec1 8841 divge0d 9733 fseq1p1m1 10089 q2submod 10380 seq3caopr2 10477 seq3distr 10508 facavg 10719 shftfibg 10822 sqrtdiv 11044 sqrtdivd 11170 mulcn2 11313 demoivreALT 11774 dvdslegcd 11957 gcdnncl 11960 qredeu 12089 rpdvds 12091 rpexp 12145 oddpwdclemodd 12164 divnumden 12188 divdenle 12189 phimullem 12217 phisum 12232 pythagtriplem4 12260 pythagtriplem8 12264 pythagtriplem9 12265 pcgcd1 12319 fldivp1 12338 pockthlem 12346 setsfun 12489 setsfun0 12490 strleund 12554 mndpropd 12773 grpidssd 12878 grpinvssd 12879 issubg2m 12980 isnsg3 12998 eqgid 13016 comet 13870 fsumcncntop 13927 mulcncf 13962 2sqlem8a 14329 2sqlem8 14330 trilpo 14651 neapmkv 14675 |
Copyright terms: Public domain | W3C validator |