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  7886  smogt  8309  inf3lem3  9551  noinfep  9581  cfsmolem  10192  genpnnp  10928  ltaddpr2  10958  fzen  13469  hashge2el2dif  14415  lcmf  16572  ncoprmlnprm  16667  prmgaplem7  16997  initoeu1  17947  termoeu1  17954  dfgrp3lem  18980  cply1mul  22252  scmataddcl  22472  scmatsubcl  22473  2ndcctbss  23411  fgcfil  25239  wilthlem3  27048  ltsval2  27636  nosupbnd1lem5  27692  cusgrsize2inds  29539  0enwwlksnge1  29949  clwlkclwwlklem2  30087  clwwlknonwwlknonb  30193  conngrv2edg  30282  pjjsi  31787  dfac21  43417  mogoldbb  48139  nnsum3primesle9  48148  evengpop3  48152  evengpoap3  48153  ztprmneprm  48701  lindslinindsimp1  48811  lindslinindsimp2lem5  48816  flnn0div2ge  48887