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 7072 f1iun 7634 odi 8194 oeoelem 8213 mapxpen 8671 xadddilem 12675 hashgt23el 13773 pcqmul 16178 infpnlem1 16234 setsn0fun 16508 chpdmat 21377 neitr 21716 hausflimi 22516 nmoix 23265 nmoleub 23267 metdsre 23388 bncssbn 23904 usgr2edg 26919 usgr2edg1 26921 crctcshwlkn0 27526 unoplin 29624 hmoplin 29646 chirredlem1 30094 mdsymlem2 30108 foresf1o 30192 ordtconnlem1 31066 signstfvn 31738 isbasisrelowllem1 34518 isbasisrelowllem2 34519 pibt2 34580 lindsadd 34766 lindsdom 34767 matunitlindflem1 34769 matunitlindflem2 34770 poimirlem25 34798 poimirlem29 34802 heicant 34808 cnambfre 34821 itg2addnclem 34824 ftc1anclem5 34852 ftc1anc 34856 rrnequiv 34994 isfldidl 35227 ispridlc 35229 supxrgelem 41481 supminfxr 41616 reccot 44785 rectan 44786 |
Copyright terms: Public domain | W3C validator |