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 257 mo4 2643 ssorduni 7489 tz7.49 8070 nneneq 8688 dfac2b 9544 qreccl 12356 dvdsaddre2b 15645 cmpsub 21936 fclsopni 22551 sumdmdlem2 30123 umgr2cycllem 32284 nocvxminlem 33144 idinside 33442 axc11n11r 33914 isbasisrelowllem1 34518 isbasisrelowllem2 34519 dmqseqim2 35771 prtlem15 35891 prtlem17 35892 ee3bir 40714 ee233 40730 onfrALTlem2 40757 ee223 40845 ee33VD 41090 rngccatidALTV 44188 ringccatidALTV 44251 |
Copyright terms: Public domain | W3C validator |