![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylanl2 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
Ref | Expression |
---|---|
sylanl2.1 | ⊢ (𝜑 → 𝜒) |
sylanl2.2 | ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
sylanl2 | ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanl2.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | 1 | anim2i 594 | . 2 ⊢ ((𝜓 ∧ 𝜑) → (𝜓 ∧ 𝜒)) |
3 | sylanl2.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylan 489 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: mpanlr1 724 adantlrl 758 adantlrr 759 oesuclem 7772 oelim 7781 mulsub 10663 divsubdiv 10931 lcmneg 15516 vdwlem12 15896 dpjidcl 18655 mplbas2 19670 monmat2matmon 20829 bwth 21413 cnextfun 22067 elbl4 22567 metucn 22575 dvradcnv 24372 dchrisum0lem2a 25403 axcontlem4 26044 cnlnadjlem2 29234 chirredlem2 29557 mdsymlem5 29573 sibfof 30709 relowlssretop 33520 matunitlindflem1 33716 poimirlem29 33749 unichnidl 34141 dmncan2 34187 cvrexchlem 35206 jm2.26 38069 radcnvrat 39013 binomcxplemnotnn0 39055 suplesup 40051 dvnmptdivc 40654 fourierdlem64 40888 fourierdlem74 40898 fourierdlem75 40899 fourierdlem83 40907 etransclem35 40987 iundjiun 41178 hoidmvlelem2 41314 |
Copyright terms: Public domain | W3C validator |