| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylanr1 | Structured version Visualization version GIF version | ||
| Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
| Ref | Expression |
|---|---|
| sylanr1.1 | ⊢ (𝜑 → 𝜒) |
| sylanr1.2 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
| Ref | Expression |
|---|---|
| sylanr1 | ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylanr1.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
| 2 | 1 | anim1i 615 | . 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜃)) |
| 3 | sylanr1.2 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
| 4 | 2, 3 | sylan2 593 | 1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: adantrll 722 adantrlr 723 sbthlem9 9131 unfi 9211 pczpre 16885 cpmadugsumlemF 22882 blsscls2 24517 rpvmasumlem 27531 leopmuli 32152 chirredlem1 32409 chirredlem3 32411 pibt2 37418 mhpind 42604 dvconstbi 44353 bccbc 44364 reccot 49277 rectan 49278 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |