![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylanl1 | Structured version Visualization version GIF version |
Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.) |
Ref | Expression |
---|---|
sylanl1.1 | ⊢ (𝜑 → 𝜓) |
sylanl1.2 | ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
sylanl1 | ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylanl1.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | anim1i 614 | . 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
3 | sylanl1.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylan 580 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: adantlll 714 adantllr 715 adantl3r 746 isocnv 6946 f1iun 7501 odi 8055 oeoelem 8074 mapxpen 8530 xadddilem 12537 hashgt23el 13633 pcqmul 16019 infpnlem1 16075 setsn0fun 16349 chpdmat 21133 neitr 21472 hausflimi 22272 nmoix 23021 nmoleub 23023 metdsre 23144 bncssbn 23660 usgr2edg 26675 usgr2edg1 26677 crctcshwlkn0 27286 unoplin 29388 hmoplin 29410 chirredlem1 29858 mdsymlem2 29872 foresf1o 29957 ordtconnlem1 30784 isbasisrelowllem1 34186 isbasisrelowllem2 34187 pibt2 34248 lindsadd 34435 lindsdom 34436 matunitlindflem1 34438 matunitlindflem2 34439 poimirlem25 34467 poimirlem29 34471 heicant 34477 cnambfre 34490 itg2addnclem 34493 ftc1anclem5 34521 ftc1anc 34525 rrnequiv 34664 isfldidl 34897 ispridlc 34899 supxrgelem 41165 supminfxr 41301 reccot 44357 rectan 44358 |
Copyright terms: Public domain | W3C validator |