![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syldc | Structured version Visualization version GIF version |
Description: Syllogism deduction. Commuted form of syld 47. (Contributed by BJ, 25-Oct-2021.) |
Ref | Expression |
---|---|
syld.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
syld.2 | ⊢ (𝜑 → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
syldc | ⊢ (𝜓 → (𝜑 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syld.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | syld.2 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜃)) | |
3 | 1, 2 | syld 47 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
4 | 3 | com12 32 | 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: nfeqf2 2371 wfrlem12OLD 8340 smogt 8387 inf3lem3 9664 noinfep 9694 cfsmolem 10302 genpnnp 11037 ltaddpr2 11067 fzen 13564 hashge2el2dif 14492 lcmf 16627 ncoprmlnprm 16723 prmgaplem7 17052 initoeu1 18026 termoeu1 18033 dfgrp3lem 19026 cply1mul 22282 scmataddcl 22504 scmatsubcl 22505 2ndcctbss 23445 fgcfil 25285 wilthlem3 27093 sltval2 27681 nosupbnd1lem5 27737 cusgrsize2inds 29385 0enwwlksnge1 29793 clwlkclwwlklem2 29928 clwwlknonwwlknonb 30034 conngrv2edg 30123 pjjsi 31628 dfac21 42762 mogoldbb 47391 nnsum3primesle9 47400 evengpop3 47404 evengpoap3 47405 ztprmneprm 47760 lindslinindsimp1 47874 lindslinindsimp2lem5 47879 flnn0div2ge 47955 |
Copyright terms: Public domain | W3C validator |