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  2377  resf1extb  7864  smogt  8287  inf3lem3  9520  noinfep  9550  cfsmolem  10158  genpnnp  10893  ltaddpr2  10923  fzen  13438  hashge2el2dif  14384  lcmf  16541  ncoprmlnprm  16636  prmgaplem7  16966  initoeu1  17915  termoeu1  17922  dfgrp3lem  18948  cply1mul  22209  scmataddcl  22429  scmatsubcl  22430  2ndcctbss  23368  fgcfil  25196  wilthlem3  27005  sltval2  27593  nosupbnd1lem5  27649  cusgrsize2inds  29430  0enwwlksnge1  29840  clwlkclwwlklem2  29975  clwwlknonwwlknonb  30081  conngrv2edg  30170  pjjsi  31675  dfac21  43098  mogoldbb  47815  nnsum3primesle9  47824  evengpop3  47828  evengpoap3  47829  ztprmneprm  48377  lindslinindsimp1  48488  lindslinindsimp2lem5  48493  flnn0div2ge  48564