![]() |
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 2375 wfrlem12OLD 8265 smogt 8312 inf3lem3 9565 noinfep 9595 cfsmolem 10205 genpnnp 10940 ltaddpr2 10970 fzen 13457 hashge2el2dif 14378 lcmf 16508 ncoprmlnprm 16602 prmgaplem7 16928 initoeu1 17896 termoeu1 17903 dfgrp3lem 18843 cply1mul 21663 scmataddcl 21863 scmatsubcl 21864 2ndcctbss 22804 fgcfil 24633 wilthlem3 26417 sltval2 27002 nosupbnd1lem5 27058 cusgrsize2inds 28399 0enwwlksnge1 28807 clwlkclwwlklem2 28942 clwwlknonwwlknonb 29048 conngrv2edg 29137 pjjsi 30640 dfac21 41371 mogoldbb 45949 nnsum3primesle9 45958 evengpop3 45962 evengpoap3 45963 ztprmneprm 46395 lindslinindsimp1 46510 lindslinindsimp2lem5 46515 flnn0div2ge 46591 |
Copyright terms: Public domain | W3C validator |