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  2380  wfrlem12OLD  8359  smogt  8406  inf3lem3  9668  noinfep  9698  cfsmolem  10308  genpnnp  11043  ltaddpr2  11073  fzen  13578  hashge2el2dif  14516  lcmf  16667  ncoprmlnprm  16762  prmgaplem7  17091  initoeu1  18065  termoeu1  18072  dfgrp3lem  19069  cply1mul  22316  scmataddcl  22538  scmatsubcl  22539  2ndcctbss  23479  fgcfil  25319  wilthlem3  27128  sltval2  27716  nosupbnd1lem5  27772  cusgrsize2inds  29486  0enwwlksnge1  29894  clwlkclwwlklem2  30029  clwwlknonwwlknonb  30135  conngrv2edg  30224  pjjsi  31729  dfac21  43055  mogoldbb  47710  nnsum3primesle9  47719  evengpop3  47723  evengpoap3  47724  ztprmneprm  48192  lindslinindsimp1  48303  lindslinindsimp2lem5  48308  flnn0div2ge  48383