Theorem syldc 49

Description: Syllogism deduction. Commuted form of syld 48. (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 48	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 33	1 ⊢ (𝜓 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  nfeqf2  2406  resf1extb  7946  smogt  8378  inf3lem3  9634  noinfep  9664  cfsmolem  10351  genpnnp  11093  ltaddpr2  11123  fzen  13677  hashge2el2dif  14628  lcmf  16813  ncoprmlnprm  16909  prmgaplem7  17240  initoeu1  18191  termoeu1  18198  dfgrp3lem  19253  cply1mul  22619  scmataddcl  22836  scmatsubcl  22837  2ndcctbss  23779  fgcfil  25597  wilthlem3  27402  ltsval2  28018  nosupbnd1lem5  28074  cusgrsize2inds  30039  0enwwlksnge1  30458  clwlkclwwlklem2  30596  clwwlknonwwlknonb  30702  conngrv2edg  30801  pjjsi  32307  onprcf1acwevdlem1  35964  dfac21  44161  mogoldbb  48976  nnsum3primesle9  48985  evengpop3  48989  evengpoap3  48990  ztprmneprm  49552  lindslinindsimp1  49662  lindslinindsimp2lem5  49667  flnn0div2ge  49738