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  2407  resf1extb  7911  smogt  8333  inf3lem3  9582  noinfep  9612  cfsmolem  10224  genpnnp  10960  ltaddpr2  10990  fzen  13543  hashge2el2dif  14490  lcmf  16650  ncoprmlnprm  16746  prmgaplem7  17076  initoeu1  18027  termoeu1  18034  dfgrp3lem  19063  cply1mul  22339  scmataddcl  22556  scmatsubcl  22557  2ndcctbss  23495  fgcfil  25313  wilthlem3  27111  ltsval2  27697  nosupbnd1lem5  27753  cusgrsize2inds  29600  0enwwlksnge1  30010  clwlkclwwlklem2  30148  clwwlknonwwlknonb  30254  conngrv2edg  30343  pjjsi  31849  dfac21  43607  mogoldbb  48371  nnsum3primesle9  48380  evengpop3  48384  evengpoap3  48385  ztprmneprm  48933  lindslinindsimp1  49043  lindslinindsimp2lem5  49048  flnn0div2ge  49119