![]() |
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: wfrlem12 7583 smogt 7621 inf3lem3 8688 noinfep 8718 cfsmolem 9255 genpnnp 9990 ltaddpr2 10020 fzen 12522 hashge2el2dif 13425 lcmf 15519 ncoprmlnprm 15609 prmgaplem7 15934 initoeu1 16833 termoeu1 16840 dfgrp3lem 17685 cply1mul 19837 scmataddcl 20495 scmatsubcl 20496 2ndcctbss 21431 fgcfil 23240 wilthlem3 24966 cusgrsize2inds 26530 0enwwlksnge1 26944 clwlkclwwlklem2 27094 clwlksfclwwlkOLD 27187 clwwlknonwwlknonb 27225 clwwlknonwwlknonbOLD 27226 conngrv2edg 27318 pjjsi 28839 sltval2 32086 nosupbnd1lem5 32135 wl-dveeq12 33593 dfac21 38107 mogoldbb 42152 nnsum3primesle9 42161 evengpop3 42165 evengpoap3 42166 ztprmneprm 42604 lindslinindsimp1 42725 lindslinindsimp2lem5 42730 flnn0div2ge 42806 |
Copyright terms: Public domain | W3C validator |