![]() |
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 | adantl 483 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
3 | sylanl2.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | syldanl 603 | 1 ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: mpanlr1 705 adantlrl 719 adantlrr 720 1stconst 8021 2ndconst 8022 oesuclem 8439 oelim 8448 undom 8937 mulsub 11532 divsubdiv 11805 lcmneg 16415 vdwlem12 16800 dpjidcl 19772 mplbas2 21371 monmat2matmon 22101 bwth 22689 cnextfun 23343 elbl4 23847 metucn 23855 dvradcnv 25708 dchrisum0lem2a 26793 axcontlem4 27721 cnlnadjlem2 30815 chirredlem2 31138 mdsymlem5 31154 sibfof 32720 relowlssretop 35765 matunitlindflem1 36005 poimirlem29 36038 unichnidl 36421 dmncan2 36467 cvrexchlem 37813 jm2.26 41228 radcnvrat 42395 binomcxplemnotnn0 42437 suplesup 43368 dvnmptdivc 43970 fourierdlem64 44202 fourierdlem74 44212 fourierdlem75 44213 fourierdlem83 44221 etransclem35 44301 iundjiun 44492 hoidmvlelem2 44628 |
Copyright terms: Public domain | W3C validator |