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  2385  wfrlem12OLD  8376  smogt  8423  inf3lem3  9699  noinfep  9729  cfsmolem  10339  genpnnp  11074  ltaddpr2  11104  fzen  13601  hashge2el2dif  14529  lcmf  16680  ncoprmlnprm  16775  prmgaplem7  17104  initoeu1  18078  termoeu1  18085  dfgrp3lem  19078  cply1mul  22321  scmataddcl  22543  scmatsubcl  22544  2ndcctbss  23484  fgcfil  25324  wilthlem3  27131  sltval2  27719  nosupbnd1lem5  27775  cusgrsize2inds  29489  0enwwlksnge1  29897  clwlkclwwlklem2  30032  clwwlknonwwlknonb  30138  conngrv2edg  30227  pjjsi  31732  dfac21  43023  mogoldbb  47659  nnsum3primesle9  47668  evengpop3  47672  evengpoap3  47673  ztprmneprm  48072  lindslinindsimp1  48186  lindslinindsimp2lem5  48191  flnn0div2ge  48267