Theorem syldc 49

Description: Syllogism deduction. Commuted form of syld 48. (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 48	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	3	com12 33	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  2411  resf1extb  7919  smogt  8342  inf3lem3  9587  noinfep  9617  cfsmolem  10242  genpnnp  10978  ltaddpr2  11008  fzen  13560  hashge2el2dif  14507  lcmf  16681  ncoprmlnprm  16777  prmgaplem7  17107  initoeu1  18058  termoeu1  18065  dfgrp3lem  19095  cply1mul  22417  scmataddcl  22634  scmatsubcl  22635  2ndcctbss  23573  fgcfil  25391  wilthlem3  27192  ltsval2  27778  nosupbnd1lem5  27834  cusgrsize2inds  29712  0enwwlksnge1  30122  clwlkclwwlklem2  30260  clwwlknonwwlknonb  30366  conngrv2edg  30455  pjjsi  31961  dfac21  43655  mogoldbb  48405  nnsum3primesle9  48414  evengpop3  48418  evengpoap3  48419  ztprmneprm  48978  lindslinindsimp1  49088  lindslinindsimp2lem5  49093  flnn0div2ge  49164