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 468 | . . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) |
4 | 1, 3 | syland 604 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
5 | 4 | ancomsd 468 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: sylan2i 607 syl2and 609 swopo 5486 wfrlem5 7961 unblem1 8772 unfi 8787 prodgt02 11490 lo1mul 14986 infpnlem1 16248 ghmcnp 22725 ulmcaulem 24984 ulmcau 24985 shintcli 29108 ballotlemfc0 31752 ballotlemfcc 31753 fprlem1 33139 frrlem15 33144 btwnxfr 33519 endofsegid 33548 bj-bary1lem1 34594 matunitlindflem1 34890 ltcvrntr 36562 poml4N 37091 |
Copyright terms: Public domain | W3C validator |