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  2376  resf1extb  7913  smogt  8339  inf3lem3  9590  noinfep  9620  cfsmolem  10230  genpnnp  10965  ltaddpr2  10995  fzen  13509  hashge2el2dif  14452  lcmf  16610  ncoprmlnprm  16705  prmgaplem7  17035  initoeu1  17980  termoeu1  17987  dfgrp3lem  18977  cply1mul  22190  scmataddcl  22410  scmatsubcl  22411  2ndcctbss  23349  fgcfil  25178  wilthlem3  26987  sltval2  27575  nosupbnd1lem5  27631  cusgrsize2inds  29388  0enwwlksnge1  29801  clwlkclwwlklem2  29936  clwwlknonwwlknonb  30042  conngrv2edg  30131  pjjsi  31636  dfac21  43062  mogoldbb  47790  nnsum3primesle9  47799  evengpop3  47803  evengpoap3  47804  ztprmneprm  48339  lindslinindsimp1  48450  lindslinindsimp2lem5  48455  flnn0div2ge  48526