![]() |
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 2339 nfeqf2OLD 2340 wfrlem12 7709 smogt 7747 inf3lem3 8824 noinfep 8854 cfsmolem 9427 genpnnp 10162 ltaddpr2 10192 fzen 12675 hashge2el2dif 13576 lcmf 15752 ncoprmlnprm 15840 prmgaplem7 16165 initoeu1 17046 termoeu1 17053 dfgrp3lem 17900 cply1mul 20060 scmataddcl 20727 scmatsubcl 20728 2ndcctbss 21667 fgcfil 23477 wilthlem3 25248 cusgrsize2inds 26801 0enwwlksnge1 27213 clwlkclwwlklem2 27380 clwwlknonwwlknonb 27508 conngrv2edg 27598 pjjsi 29131 sltval2 32398 nosupbnd1lem5 32447 dfac21 38595 mogoldbb 42698 nnsum3primesle9 42707 evengpop3 42711 evengpoap3 42712 ztprmneprm 43140 lindslinindsimp1 43261 lindslinindsimp2lem5 43266 flnn0div2ge 43342 |
Copyright terms: Public domain | W3C validator |