![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl31anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
syl31anc.5 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
Ref | Expression |
---|---|
syl31anc | ⊢ (𝜑 → 𝜂) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1178 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | sylXanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl31anc.5 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) | |
7 | 4, 5, 6 | syl2anc 411 | 1 ⊢ (𝜑 → 𝜂) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 979 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 981 |
This theorem is referenced by: syl32anc 1256 stoic4b 1443 enq0tr 7447 ltmul12a 8831 lt2msq1 8856 ledivp1 8874 lemul1ad 8910 lemul2ad 8911 lediv2ad 9733 xaddge0 9892 difelfznle 10149 expubnd 10591 nn0leexp2 10704 expcanlem 10709 expcand 10711 xrmaxaddlem 11282 mertenslemi1 11557 eftlub 11712 dvdsadd 11857 divalgmod 11946 gcdzeq 12037 rplpwr 12042 sqgcd 12044 bezoutr 12047 rpmulgcd2 12109 rpdvds 12113 isprm5 12156 divgcdodd 12157 oddpwdclemxy 12183 divnumden 12210 crth 12238 phimullem 12239 coprimeprodsq2 12272 pythagtriplem19 12296 pclemub 12301 pcpre1 12306 pcidlem 12336 pockthlem 12368 prmunb 12374 kerf1ghm 13168 xblss2ps 14257 xblss2 14258 metcnpi3 14370 limcimolemlt 14486 limccnp2cntop 14499 dvmulxxbr 14519 dvcoapbr 14524 2lgsoddprmlem1 14806 2sqlem8a 14822 2sqlem8 14823 |
Copyright terms: Public domain | W3C validator |