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  2391  wfrlem12  7960  smogt  7998  inf3lem3  9087  noinfep  9117  cfsmolem  9686  genpnnp  10421  ltaddpr2  10451  fzen  12918  hashge2el2dif  13832  lcmf  15971  ncoprmlnprm  16062  prmgaplem7  16387  initoeu1  17265  termoeu1  17272  dfgrp3lem  18191  cply1mul  20456  scmataddcl  21119  scmatsubcl  21120  2ndcctbss  22057  fgcfil  23868  wilthlem3  25641  cusgrsize2inds  27229  0enwwlksnge1  27636  clwlkclwwlklem2  27772  clwwlknonwwlknonb  27879  conngrv2edg  27968  pjjsi  29471  sltval2  33158  nosupbnd1lem5  33207  dfac21  39659  mogoldbb  43943  nnsum3primesle9  43952  evengpop3  43956  evengpoap3  43957  ztprmneprm  44388  lindslinindsimp1  44505  lindslinindsimp2lem5  44510  flnn0div2ge  44586