Theorem syldc 48

Description: Syllogism deduction. Commuted form of syld 47. (Contributed by BJ, 25-Oct-2021.)

Hypotheses

Ref	Expression
syld.1	⊢ (𝜑 → (𝜓 → 𝜒))
syld.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
syldc	⊢ (𝜓 → (𝜑 → 𝜃))

Proof of Theorem syldc

Step	Hyp	Ref	Expression
1		syld.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	1, 2	syld 47	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 32	1 ⊢ (𝜓 → (𝜑 → 𝜃))

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  resf1extb  7910  smogt  8336  inf3lem3  9583  noinfep  9613  cfsmolem  10223  genpnnp  10958  ltaddpr2  10988  fzen  13502  hashge2el2dif  14445  lcmf  16603  ncoprmlnprm  16698  prmgaplem7  17028  initoeu1  17973  termoeu1  17980  dfgrp3lem  18970  cply1mul  22183  scmataddcl  22403  scmatsubcl  22404  2ndcctbss  23342  fgcfil  25171  wilthlem3  26980  sltval2  27568  nosupbnd1lem5  27624  cusgrsize2inds  29381  0enwwlksnge1  29794  clwlkclwwlklem2  29929  clwwlknonwwlknonb  30035  conngrv2edg  30124  pjjsi  31629  dfac21  43055  mogoldbb  47786  nnsum3primesle9  47795  evengpop3  47799  evengpoap3  47800  ztprmneprm  48335  lindslinindsimp1  48446  lindslinindsimp2lem5  48451  flnn0div2ge  48522