![]() |
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 8772 divcanap5d 8773 divcanap7d 8775 divdivap1d 8778 divdivap2d 8779 seq3coll 10821 cau3lem 11122 summodclem2a 11388 prodmodclem2a 11583 prmind2 12119 divnumden 12195 pceulem 12293 pcqmul 12302 pcqdiv 12306 pcexp 12308 pcaddlem 12337 pcbc 12348 abladdsub4 13115 ablpnpcan 13121 lmodvs1 13404 blss2ps 13876 blss2 13877 blssps 13897 blss 13898 xmeter 13906 lgsdi 14408 |
Copyright terms: Public domain | W3C validator |