| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl8 | Structured version Visualization version GIF version | ||
| Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) |
| Ref | Expression |
|---|---|
| syl8.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| syl8.2 | ⊢ (𝜃 → 𝜏) |
| Ref | Expression |
|---|---|
| syl8 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl8.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
| 2 | syl8.2 | . . 3 ⊢ (𝜃 → 𝜏) | |
| 3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) |
| 4 | 1, 3 | syl6d 75 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
| This theorem is referenced by: a1ddd 80 com45 97 syl8ib 256 mo4 2566 ssorduni 7799 tz7.49 8485 nneneq 9246 nneneqOLD 9258 dfac2b 10171 qreccl 13011 dvdsaddre2b 16344 cmpsub 23408 fclsopni 24023 nocvxminlem 27822 sumdmdlem2 32438 umgr2cycllem 35145 idinside 36085 axc11n11r 36684 isbasisrelowllem1 37356 isbasisrelowllem2 37357 dmqseqim2 38658 disjlem17 38800 prtlem15 38876 prtlem17 38877 ee3bir 44523 ee233 44539 onfrALTlem2 44566 ee223 44654 ee33VD 44899 ormkglobd 46890 rngccatidALTV 48188 ringccatidALTV 48222 |
| Copyright terms: Public domain | W3C validator |