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  2452  wfrlem12  7583  smogt  7621  inf3lem3  8695  noinfep  8725  cfsmolem  9298  genpnnp  10033  ltaddpr2  10063  fzen  12565  hashge2el2dif  13464  lcmf  15554  ncoprmlnprm  15643  prmgaplem7  15968  initoeu1  16868  termoeu1  16875  dfgrp3lem  17721  cply1mul  19879  scmataddcl  20540  scmatsubcl  20541  2ndcctbss  21479  fgcfil  23288  wilthlem3  25017  cusgrsize2inds  26584  0enwwlksnge1  26998  clwlkclwwlklem2  27150  clwlksfclwwlkOLD  27243  clwwlknonwwlknonb  27281  clwwlknonwwlknonbOLD  27282  conngrv2edg  27375  pjjsi  28899  sltval2  32146  nosupbnd1lem5  32195  dfac21  38160  mogoldbb  42196  nnsum3primesle9  42205  evengpop3  42209  evengpoap3  42210  ztprmneprm  42648  lindslinindsimp1  42769  lindslinindsimp2lem5  42774  flnn0div2ge  42850