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 590 | . 2 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
3 | sylanl1.2 | . 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
4 | 2, 3 | sylan 487 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: adantlll 750 adantllr 751 isocnv 6480 odi 7546 oeoelem 7565 mapxpen 8011 xadddilem 11996 pcqmul 15396 infpnlem1 15452 chpdmat 20465 neitr 20794 hausflimi 21594 nmoix 22343 nmoleub 22345 metdsre 22464 pthdepisspth 26104 extwwlkfab 26617 sspph 27094 unoplin 28163 hmoplin 28185 chirredlem1 28633 mdsymlem2 28647 foresf1o 28727 ordtconlem1 29298 isbasisrelowllem1 32379 isbasisrelowllem2 32380 lindsdom 32573 matunitlindflem1 32575 matunitlindflem2 32576 poimirlem25 32604 poimirlem29 32608 heicant 32614 cnambfre 32628 itg2addnclem 32631 ftc1anclem5 32659 ftc1anc 32663 rrnequiv 32804 isfldidl 33037 ispridlc 33039 supxrgelem 38494 usgr2edg1 40439 crctcsh1wlkn0 41024 reccot 42298 rectan 42299 |
Copyright terms: Public domain | W3C validator |