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 ⊢ (𝜓 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  nfeqf2  2408  resf1extb  7935  smogt  8360  inf3lem3  9613  noinfep  9643  cfsmolem  10276  genpnnp  11018  ltaddpr2  11048  fzen  13599  hashge2el2dif  14549  lcmf  16729  ncoprmlnprm  16825  prmgaplem7  17155  initoeu1  18106  termoeu1  18113  dfgrp3lem  19167  cply1mul  22527  scmataddcl  22744  scmatsubcl  22745  2ndcctbss  23687  fgcfil  25505  wilthlem3  27314  ltsval2  27900  nosupbnd1lem5  27956  cusgrsize2inds  29921  0enwwlksnge1  30340  clwlkclwwlklem2  30478  clwwlknonwwlknonb  30584  conngrv2edg  30683  pjjsi  32189  dfac21  43915  mogoldbb  48709  nnsum3primesle9  48718  evengpop3  48722  evengpoap3  48723  ztprmneprm  49285  lindslinindsimp1  49395  lindslinindsimp2lem5  49400  flnn0div2ge  49471