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 4236 brcogw 4703 funprg 5168 funtpg 5169 fnunsn 5225 ftpg 5597 fsnunf 5613 isotr 5710 off 5987 caofrss 5999 tfr1onlembxssdm 6233 tfrcllembxssdm 6246 pmresg 6563 ac6sfi 6785 tridc 6786 fidcenumlemrks 6834 sbthlemi8 6845 casefun 6963 caseinj 6967 djufun 6982 djuinj 6984 mulclpi 7129 archnqq 7218 addlocprlemlt 7332 addlocprlemeq 7334 addlocprlemgt 7335 mullocprlem 7371 apreim 8358 subrecap 8591 ltrec1 8639 divge0d 9517 fseq1p1m1 9867 q2submod 10151 seq3caopr2 10248 seq3distr 10279 facavg 10485 shftfibg 10585 sqrtdiv 10807 sqrtdivd 10933 mulcn2 11074 demoivreALT 11469 dvdslegcd 11642 gcdnncl 11645 qredeu 11767 rpdvds 11769 rpexp 11820 oddpwdclemodd 11839 divnumden 11863 divdenle 11864 phimullem 11890 setsfun 11983 setsfun0 11984 strleund 12036 comet 12657 fsumcncntop 12714 mulcncf 12749 trilpo 13225 |
Copyright terms: Public domain | W3C validator |