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 307 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
5 | syl21anc.4 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
6 | 4, 5 | syl 14 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: issod 4304 brcogw 4780 funprg 5248 funtpg 5249 fnunsn 5305 ftpg 5680 fsnunf 5696 isotr 5795 off 6073 caofrss 6085 tfr1onlembxssdm 6322 tfrcllembxssdm 6335 pmresg 6654 ac6sfi 6876 tridc 6877 fidcenumlemrks 6930 sbthlemi8 6941 casefun 7062 caseinj 7066 djufun 7081 djuinj 7083 mulclpi 7290 archnqq 7379 addlocprlemlt 7493 addlocprlemeq 7495 addlocprlemgt 7496 mullocprlem 7532 apreim 8522 subrecap 8756 ltrec1 8804 divge0d 9694 fseq1p1m1 10050 q2submod 10341 seq3caopr2 10438 seq3distr 10469 facavg 10680 shftfibg 10784 sqrtdiv 11006 sqrtdivd 11132 mulcn2 11275 demoivreALT 11736 dvdslegcd 11919 gcdnncl 11922 qredeu 12051 rpdvds 12053 rpexp 12107 oddpwdclemodd 12126 divnumden 12150 divdenle 12151 phimullem 12179 phisum 12194 pythagtriplem4 12222 pythagtriplem8 12226 pythagtriplem9 12227 pcgcd1 12281 fldivp1 12300 pockthlem 12308 setsfun 12451 setsfun0 12452 strleund 12506 mndpropd 12676 comet 13293 fsumcncntop 13350 mulcncf 13385 2sqlem8a 13752 2sqlem8 13753 trilpo 14075 neapmkv 14099 |
Copyright terms: Public domain | W3C validator |