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  2375  resf1extb  7874  smogt  8297  inf3lem3  9545  noinfep  9575  cfsmolem  10183  genpnnp  10918  ltaddpr2  10948  fzen  13462  hashge2el2dif  14405  lcmf  16562  ncoprmlnprm  16657  prmgaplem7  16987  initoeu1  17936  termoeu1  17943  dfgrp3lem  18935  cply1mul  22199  scmataddcl  22419  scmatsubcl  22420  2ndcctbss  23358  fgcfil  25187  wilthlem3  26996  sltval2  27584  nosupbnd1lem5  27640  cusgrsize2inds  29417  0enwwlksnge1  29827  clwlkclwwlklem2  29962  clwwlknonwwlknonb  30068  conngrv2edg  30157  pjjsi  31662  dfac21  43039  mogoldbb  47770  nnsum3primesle9  47779  evengpop3  47783  evengpoap3  47784  ztprmneprm  48332  lindslinindsimp1  48443  lindslinindsimp2lem5  48448  flnn0div2ge  48519