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  2382  resf1extb  7878  smogt  8300  inf3lem3  9542  noinfep  9572  cfsmolem  10183  genpnnp  10919  ltaddpr2  10949  fzen  13486  hashge2el2dif  14433  lcmf  16593  ncoprmlnprm  16689  prmgaplem7  17019  initoeu1  17969  termoeu1  17976  dfgrp3lem  19005  cply1mul  22271  scmataddcl  22491  scmatsubcl  22492  2ndcctbss  23430  fgcfil  25248  wilthlem3  27047  ltsval2  27634  nosupbnd1lem5  27690  cusgrsize2inds  29537  0enwwlksnge1  29947  clwlkclwwlklem2  30085  clwwlknonwwlknonb  30191  conngrv2edg  30280  pjjsi  31786  dfac21  43512  mogoldbb  48273  nnsum3primesle9  48282  evengpop3  48286  evengpoap3  48287  ztprmneprm  48835  lindslinindsimp1  48945  lindslinindsimp2lem5  48950  flnn0div2ge  49021