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  resf1extb  7881  smogt  8304  inf3lem3  9549  noinfep  9579  cfsmolem  10190  genpnnp  10926  ltaddpr2  10956  fzen  13493  hashge2el2dif  14440  lcmf  16600  ncoprmlnprm  16696  prmgaplem7  17026  initoeu1  17976  termoeu1  17983  dfgrp3lem  19012  cply1mul  22289  scmataddcl  22506  scmatsubcl  22507  2ndcctbss  23445  fgcfil  25263  wilthlem3  27058  ltsval2  27645  nosupbnd1lem5  27701  cusgrsize2inds  29547  0enwwlksnge1  29957  clwlkclwwlklem2  30095  clwwlknonwwlknonb  30201  conngrv2edg  30290  pjjsi  31796  dfac21  43518  mogoldbb  48283  nnsum3primesle9  48292  evengpop3  48296  evengpoap3  48297  ztprmneprm  48845  lindslinindsimp1  48955  lindslinindsimp2lem5  48960  flnn0div2ge  49031