|   | 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 2381 resf1extb 7957 wfrlem12OLD 8361 smogt 8408 inf3lem3 9671 noinfep 9701 cfsmolem 10311 genpnnp 11046 ltaddpr2 11076 fzen 13582 hashge2el2dif 14520 lcmf 16671 ncoprmlnprm 16766 prmgaplem7 17096 initoeu1 18057 termoeu1 18064 dfgrp3lem 19057 cply1mul 22301 scmataddcl 22523 scmatsubcl 22524 2ndcctbss 23464 fgcfil 25306 wilthlem3 27114 sltval2 27702 nosupbnd1lem5 27758 cusgrsize2inds 29472 0enwwlksnge1 29885 clwlkclwwlklem2 30020 clwwlknonwwlknonb 30126 conngrv2edg 30215 pjjsi 31720 dfac21 43083 mogoldbb 47777 nnsum3primesle9 47786 evengpop3 47790 evengpoap3 47791 ztprmneprm 48268 lindslinindsimp1 48379 lindslinindsimp2lem5 48384 flnn0div2ge 48459 | 
| Copyright terms: Public domain | W3C validator |