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  2377  wfrlem12OLD  8151  smogt  8198  inf3lem3  9388  noinfep  9418  cfsmolem  10026  genpnnp  10761  ltaddpr2  10791  fzen  13273  hashge2el2dif  14194  lcmf  16338  ncoprmlnprm  16432  prmgaplem7  16758  initoeu1  17726  termoeu1  17733  dfgrp3lem  18673  cply1mul  21465  scmataddcl  21665  scmatsubcl  21666  2ndcctbss  22606  fgcfil  24435  wilthlem3  26219  cusgrsize2inds  27820  0enwwlksnge1  28229  clwlkclwwlklem2  28364  clwwlknonwwlknonb  28470  conngrv2edg  28559  pjjsi  30062  sltval2  33859  nosupbnd1lem5  33915  dfac21  40891  mogoldbb  45237  nnsum3primesle9  45246  evengpop3  45250  evengpoap3  45251  ztprmneprm  45683  lindslinindsimp1  45798  lindslinindsimp2lem5  45803  flnn0div2ge  45879