![]() |
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 8773 divcanap5d 8774 divcanap7d 8776 divdivap1d 8779 divdivap2d 8780 seq3coll 10822 cau3lem 11123 summodclem2a 11389 prodmodclem2a 11584 prmind2 12120 divnumden 12196 pceulem 12294 pcqmul 12303 pcqdiv 12307 pcexp 12309 pcaddlem 12338 pcbc 12349 abladdsub4 13117 ablpnpcan 13123 lmodvs1 13406 blss2ps 13909 blss2 13910 blssps 13930 blss 13931 xmeter 13939 lgsdi 14441 |
Copyright terms: Public domain | W3C validator |