| 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 481 | . 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
| 3 | sylanl2.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
| 4 | 2, 3 | syldanl 602 | 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: mpanlr1 706 adantlrl 720 adantlrr 721 1stconst 8125 2ndconst 8126 oesuclem 8563 oelim 8572 undom 9099 mulsub 11706 divsubdiv 11983 lcmneg 16640 vdwlem12 17030 dpjidcl 20078 mplbas2 22060 monmat2matmon 22830 bwth 23418 cnextfun 24072 elbl4 24576 metucn 24584 dvradcnv 26464 dchrisum0lem2a 27561 axcontlem4 28982 cnlnadjlem2 32087 chirredlem2 32410 mdsymlem5 32426 sibfof 34342 relowlssretop 37364 matunitlindflem1 37623 poimirlem29 37656 unichnidl 38038 dmncan2 38084 cvrexchlem 39421 evlsvvval 42573 jm2.26 43014 radcnvrat 44333 binomcxplemnotnn0 44375 suplesup 45350 dvnmptdivc 45953 fourierdlem64 46185 fourierdlem74 46195 fourierdlem75 46196 fourierdlem83 46204 etransclem35 46284 iundjiun 46475 hoidmvlelem2 46611 |
| Copyright terms: Public domain | W3C validator |