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  7935  wfrlem12OLD  8339  smogt  8386  inf3lem3  9649  noinfep  9679  cfsmolem  10289  genpnnp  11024  ltaddpr2  11054  fzen  13563  hashge2el2dif  14503  lcmf  16657  ncoprmlnprm  16752  prmgaplem7  17082  initoeu1  18029  termoeu1  18036  dfgrp3lem  19026  cply1mul  22239  scmataddcl  22459  scmatsubcl  22460  2ndcctbss  23398  fgcfil  25228  wilthlem3  27037  sltval2  27625  nosupbnd1lem5  27681  cusgrsize2inds  29438  0enwwlksnge1  29851  clwlkclwwlklem2  29986  clwwlknonwwlknonb  30092  conngrv2edg  30181  pjjsi  31686  dfac21  43057  mogoldbb  47766  nnsum3primesle9  47775  evengpop3  47779  evengpoap3  47780  ztprmneprm  48289  lindslinindsimp1  48400  lindslinindsimp2lem5  48405  flnn0div2ge  48480