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  7885  smogt  8307  inf3lem3  9551  noinfep  9581  cfsmolem  10192  genpnnp  10928  ltaddpr2  10958  fzen  13495  hashge2el2dif  14442  lcmf  16602  ncoprmlnprm  16698  prmgaplem7  17028  initoeu1  17978  termoeu1  17985  dfgrp3lem  19014  cply1mul  22261  scmataddcl  22481  scmatsubcl  22482  2ndcctbss  23420  fgcfil  25238  wilthlem3  27033  ltsval2  27620  nosupbnd1lem5  27676  cusgrsize2inds  29522  0enwwlksnge1  29932  clwlkclwwlklem2  30070  clwwlknonwwlknonb  30176  conngrv2edg  30265  pjjsi  31771  dfac21  43494  mogoldbb  48261  nnsum3primesle9  48270  evengpop3  48274  evengpoap3  48275  ztprmneprm  48823  lindslinindsimp1  48933  lindslinindsimp2lem5  48938  flnn0div2ge  49009