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  2379  resf1extb  7870  smogt  8293  inf3lem3  9527  noinfep  9557  cfsmolem  10168  genpnnp  10903  ltaddpr2  10933  fzen  13443  hashge2el2dif  14389  lcmf  16546  ncoprmlnprm  16641  prmgaplem7  16971  initoeu1  17920  termoeu1  17927  dfgrp3lem  18953  cply1mul  22212  scmataddcl  22432  scmatsubcl  22433  2ndcctbss  23371  fgcfil  25199  wilthlem3  27008  sltval2  27596  nosupbnd1lem5  27652  cusgrsize2inds  29434  0enwwlksnge1  29844  clwlkclwwlklem2  29982  clwwlknonwwlknonb  30088  conngrv2edg  30177  pjjsi  31682  dfac21  43183  mogoldbb  47909  nnsum3primesle9  47918  evengpop3  47922  evengpoap3  47923  ztprmneprm  48471  lindslinindsimp1  48582  lindslinindsimp2lem5  48587  flnn0div2ge  48658