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 ⊢ (𝜓 → (𝜑 → 𝜃))

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  2409  resf1extb  7932  smogt  8355  inf3lem3  9600  noinfep  9630  cfsmolem  10255  genpnnp  10991  ltaddpr2  11021  fzen  13570  hashge2el2dif  14519  lcmf  16692  ncoprmlnprm  16788  prmgaplem7  17118  initoeu1  18069  termoeu1  18076  dfgrp3lem  19105  cply1mul  22437  scmataddcl  22654  scmatsubcl  22655  2ndcctbss  23593  fgcfil  25411  wilthlem3  27212  ltsval2  27798  nosupbnd1lem5  27854  cusgrsize2inds  29781  0enwwlksnge1  30191  clwlkclwwlklem2  30329  clwwlknonwwlknonb  30435  conngrv2edg  30524  pjjsi  32030  dfac21  43773  mogoldbb  48527  nnsum3primesle9  48536  evengpop3  48540  evengpoap3  48541  ztprmneprm  49104  lindslinindsimp1  49214  lindslinindsimp2lem5  49219  flnn0div2ge  49290