| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sylan2d | Structured version Visualization version GIF version | ||
| Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
| Ref | Expression |
|---|---|
| sylan2d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| sylan2d.2 | ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏)) |
| Ref | Expression |
|---|---|
| sylan2d | ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sylan2d.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | sylan2d.2 | . . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏)) | |
| 3 | 2 | ancomsd 465 | . . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) |
| 4 | 1, 3 | syland 603 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
| 5 | 4 | ancomsd 465 | 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: sylan2i 606 syl2and 608 swopo 5603 fprlem1 8325 wfrlem5OLD 8353 unblem1 9328 frrlem15 9797 prodgt02 12115 lo1mul 15664 infpnlem1 16948 ghmcnp 24123 ulmcaulem 26437 ulmcau 26438 shintcli 31348 ballotlemfc0 34495 ballotlemfcc 34496 btwnxfr 36057 endofsegid 36086 bj-bary1lem1 37312 matunitlindflem1 37623 ltcvrntr 39426 poml4N 39955 |
| Copyright terms: Public domain | W3C validator |