![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2ani | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
Ref | Expression |
---|---|
syl2ani.1 | ⊢ (𝜑 → 𝜒) |
syl2ani.2 | ⊢ (𝜂 → 𝜃) |
syl2ani.3 | ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
syl2ani | ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2ani.1 | . 2 ⊢ (𝜑 → 𝜒) | |
2 | syl2ani.2 | . . 3 ⊢ (𝜂 → 𝜃) | |
3 | syl2ani.3 | . . 3 ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) | |
4 | 2, 3 | sylan2i 606 | . 2 ⊢ (𝜓 → ((𝜒 ∧ 𝜂) → 𝜏)) |
5 | 1, 4 | sylani 604 | 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: 2mo 2645 fvf1pr 7326 frxp 8149 poxp2 8166 mapen 9179 rex2dom 9279 fin1a2lem9 10445 coprmproddvdslem 16695 psss 18637 mgmidmo 18685 aannenlem1 26384 funtransport 36012 cgrxfr 36036 btwnxfr 36037 weiunpo 36447 bj-cbv3tb 36769 |
Copyright terms: Public domain | W3C validator |