![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl122anc | GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
sylXanc.1 | ⊢ (𝜑 → 𝜓) |
sylXanc.2 | ⊢ (𝜑 → 𝜒) |
sylXanc.3 | ⊢ (𝜑 → 𝜃) |
sylXanc.4 | ⊢ (𝜑 → 𝜏) |
sylXanc.5 | ⊢ (𝜑 → 𝜂) |
syl122anc.6 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) |
Ref | Expression |
---|---|
syl122anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylXanc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | sylXanc.2 | . 2 ⊢ (𝜑 → 𝜒) | |
3 | sylXanc.3 | . 2 ⊢ (𝜑 → 𝜃) | |
4 | sylXanc.4 | . . 3 ⊢ (𝜑 → 𝜏) | |
5 | sylXanc.5 | . . 3 ⊢ (𝜑 → 𝜂) | |
6 | 4, 5 | jca 306 | . 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂)) |
7 | syl122anc.6 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) | |
8 | 1, 2, 3, 6, 7 | syl121anc 1243 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 978 |
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 980 |
This theorem is referenced by: divdiv32apd 8749 divcanap5d 8750 divcanap7d 8752 divdivap1d 8755 divdivap2d 8756 seq3coll 10793 cau3lem 11094 summodclem2a 11360 prodmodclem2a 11555 prmind2 12090 divnumden 12166 pceulem 12264 pcqmul 12273 pcqdiv 12277 pcexp 12279 pcaddlem 12308 pcbc 12319 abladdsub4 12931 ablpnpcan 12937 blss2ps 13539 blss2 13540 blssps 13560 blss 13561 xmeter 13569 lgsdi 14071 |
Copyright terms: Public domain | W3C validator |