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  2339  nfeqf2OLD  2340  wfrlem12  7709  smogt  7747  inf3lem3  8824  noinfep  8854  cfsmolem  9427  genpnnp  10162  ltaddpr2  10192  fzen  12675  hashge2el2dif  13576  lcmf  15752  ncoprmlnprm  15840  prmgaplem7  16165  initoeu1  17046  termoeu1  17053  dfgrp3lem  17900  cply1mul  20060  scmataddcl  20727  scmatsubcl  20728  2ndcctbss  21667  fgcfil  23477  wilthlem3  25248  cusgrsize2inds  26801  0enwwlksnge1  27213  clwlkclwwlklem2  27380  clwwlknonwwlknonb  27508  conngrv2edg  27598  pjjsi  29131  sltval2  32398  nosupbnd1lem5  32447  dfac21  38595  mogoldbb  42698  nnsum3primesle9  42707  evengpop3  42711  evengpoap3  42712  ztprmneprm  43140  lindslinindsimp1  43261  lindslinindsimp2lem5  43266  flnn0div2ge  43342