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  2376  resf1extb  7912  smogt  8338  inf3lem3  9589  noinfep  9619  cfsmolem  10229  genpnnp  10964  ltaddpr2  10994  fzen  13508  hashge2el2dif  14451  lcmf  16609  ncoprmlnprm  16704  prmgaplem7  17034  initoeu1  17979  termoeu1  17986  dfgrp3lem  18976  cply1mul  22189  scmataddcl  22409  scmatsubcl  22410  2ndcctbss  23348  fgcfil  25177  wilthlem3  26986  sltval2  27574  nosupbnd1lem5  27630  cusgrsize2inds  29387  0enwwlksnge1  29800  clwlkclwwlklem2  29935  clwwlknonwwlknonb  30041  conngrv2edg  30130  pjjsi  31635  dfac21  43048  mogoldbb  47776  nnsum3primesle9  47785  evengpop3  47789  evengpoap3  47790  ztprmneprm  48325  lindslinindsimp1  48436  lindslinindsimp2lem5  48441  flnn0div2ge  48512