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 2386 wfrlem12 7955 smogt 7993 inf3lem3 9081 noinfep 9111 cfsmolem 9680 genpnnp 10415 ltaddpr2 10445 fzen 12912 hashge2el2dif 13826 lcmf 15965 ncoprmlnprm 16056 prmgaplem7 16381 initoeu1 17259 termoeu1 17266 dfgrp3lem 18135 cply1mul 20390 scmataddcl 21053 scmatsubcl 21054 2ndcctbss 21991 fgcfil 23801 wilthlem3 25574 cusgrsize2inds 27162 0enwwlksnge1 27569 clwlkclwwlklem2 27705 clwwlknonwwlknonb 27812 conngrv2edg 27901 pjjsi 29404 sltval2 33060 nosupbnd1lem5 33109 dfac21 39544 mogoldbb 43827 nnsum3primesle9 43836 evengpop3 43840 evengpoap3 43841 ztprmneprm 44323 lindslinindsimp1 44440 lindslinindsimp2lem5 44445 flnn0div2ge 44521 |
Copyright terms: Public domain | W3C validator |