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  2381  resf1extb  7957  wfrlem12OLD  8361  smogt  8408  inf3lem3  9671  noinfep  9701  cfsmolem  10311  genpnnp  11046  ltaddpr2  11076  fzen  13582  hashge2el2dif  14520  lcmf  16671  ncoprmlnprm  16766  prmgaplem7  17096  initoeu1  18057  termoeu1  18064  dfgrp3lem  19057  cply1mul  22301  scmataddcl  22523  scmatsubcl  22524  2ndcctbss  23464  fgcfil  25306  wilthlem3  27114  sltval2  27702  nosupbnd1lem5  27758  cusgrsize2inds  29472  0enwwlksnge1  29885  clwlkclwwlklem2  30020  clwwlknonwwlknonb  30126  conngrv2edg  30215  pjjsi  31720  dfac21  43083  mogoldbb  47777  nnsum3primesle9  47786  evengpop3  47790  evengpoap3  47791  ztprmneprm  48268  lindslinindsimp1  48379  lindslinindsimp2lem5  48384  flnn0div2ge  48459