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  2381  resf1extb  7876  smogt  8299  inf3lem3  9539  noinfep  9569  cfsmolem  10180  genpnnp  10916  ltaddpr2  10946  fzen  13457  hashge2el2dif  14403  lcmf  16560  ncoprmlnprm  16655  prmgaplem7  16985  initoeu1  17935  termoeu1  17942  dfgrp3lem  18968  cply1mul  22240  scmataddcl  22460  scmatsubcl  22461  2ndcctbss  23399  fgcfil  25227  wilthlem3  27036  ltsval2  27624  nosupbnd1lem5  27680  cusgrsize2inds  29527  0enwwlksnge1  29937  clwlkclwwlklem2  30075  clwwlknonwwlknonb  30181  conngrv2edg  30270  pjjsi  31775  dfac21  43304  mogoldbb  48027  nnsum3primesle9  48036  evengpop3  48040  evengpoap3  48041  ztprmneprm  48589  lindslinindsimp1  48699  lindslinindsimp2lem5  48704  flnn0div2ge  48775