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 616 | . 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
3 | sylanl1.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylan 582 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: adantlll 716 adantllr 717 adantl3r 748 isocnv 7075 f1iun 7637 odi 8197 oeoelem 8216 mapxpen 8675 xadddilem 12679 hashgt23el 13777 pcqmul 16182 infpnlem1 16238 setsn0fun 16512 chpdmat 21441 neitr 21780 hausflimi 22580 nmoix 23330 nmoleub 23332 metdsre 23453 bncssbn 23969 usgr2edg 26984 usgr2edg1 26986 crctcshwlkn0 27591 unoplin 29689 hmoplin 29711 chirredlem1 30159 mdsymlem2 30173 foresf1o 30257 ordtconnlem1 31160 signstfvn 31832 isbasisrelowllem1 34628 isbasisrelowllem2 34629 pibt2 34690 lindsadd 34877 lindsdom 34878 matunitlindflem1 34880 matunitlindflem2 34881 poimirlem25 34909 poimirlem29 34913 heicant 34919 cnambfre 34932 itg2addnclem 34935 ftc1anclem5 34963 ftc1anc 34967 rrnequiv 35105 isfldidl 35338 ispridlc 35340 supxrgelem 41595 supminfxr 41730 reccot 44848 rectan 44849 |
Copyright terms: Public domain | W3C validator |