![]() |
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 2561 ssorduni 7763 tz7.49 8442 nneneq 9206 nneneqOLD 9218 dfac2b 10122 qreccl 12950 dvdsaddre2b 16247 cmpsub 22896 fclsopni 23511 nocvxminlem 27269 sumdmdlem2 31660 umgr2cycllem 34120 idinside 35045 axc11n11r 35550 isbasisrelowllem1 36225 isbasisrelowllem2 36226 dmqseqim2 37516 disjlem17 37658 prtlem15 37734 prtlem17 37735 ee3bir 43250 ee233 43266 onfrALTlem2 43293 ee223 43381 ee33VD 43626 rngccatidALTV 46841 ringccatidALTV 46904 |
Copyright terms: Public domain | W3C validator |