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  2412  resf1extb  7940  smogt  8363  inf3lem3  9609  noinfep  9639  cfsmolem  10272  genpnnp  11008  ltaddpr2  11038  fzen  13587  hashge2el2dif  14537  lcmf  16716  ncoprmlnprm  16812  prmgaplem7  17142  initoeu1  18093  termoeu1  18100  dfgrp3lem  19135  cply1mul  22493  scmataddcl  22710  scmatsubcl  22711  2ndcctbss  23649  fgcfil  25467  wilthlem3  27271  ltsval2  27857  nosupbnd1lem5  27913  cusgrsize2inds  29840  0enwwlksnge1  30250  clwlkclwwlklem2  30388  clwwlknonwwlknonb  30494  conngrv2edg  30583  pjjsi  32089  dfac21  43834  mogoldbb  48591  nnsum3primesle9  48600  evengpop3  48604  evengpoap3  48605  ztprmneprm  49168  lindslinindsimp1  49278  lindslinindsimp2lem5  49283  flnn0div2ge  49354