![]() |
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 609 | . 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
3 | sylanl1.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylan 576 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 |
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 199 df-an 386 |
This theorem is referenced by: adantlll 710 adantllr 711 isocnv 6806 odi 7897 oeoelem 7916 mapxpen 8366 xadddilem 12369 pcqmul 15888 infpnlem1 15944 setsn0fun 16218 chpdmat 20971 neitr 21310 hausflimi 22109 nmoix 22858 nmoleub 22860 metdsre 22981 bncssbn 23497 usgr2edg1 26437 crctcshwlkn0 27064 sspphOLD 28227 unoplin 29296 hmoplin 29318 chirredlem1 29766 mdsymlem2 29780 foresf1o 29853 ordtconnlem1 30478 isbasisrelowllem1 33693 isbasisrelowllem2 33694 lindsdom 33884 matunitlindflem1 33886 matunitlindflem2 33887 poimirlem25 33915 poimirlem29 33919 heicant 33925 cnambfre 33938 itg2addnclem 33941 ftc1anclem5 33969 ftc1anc 33973 rrnequiv 34113 isfldidl 34346 ispridlc 34348 supxrgelem 40285 supminfxr 40425 reccot 43289 rectan 43290 |
Copyright terms: Public domain | W3C validator |