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  wfrlem12OLD  8122  smogt  8169  inf3lem3  9318  noinfep  9348  cfsmolem  9957  genpnnp  10692  ltaddpr2  10722  fzen  13202  hashge2el2dif  14122  lcmf  16266  ncoprmlnprm  16360  prmgaplem7  16686  initoeu1  17642  termoeu1  17649  dfgrp3lem  18588  cply1mul  21375  scmataddcl  21573  scmatsubcl  21574  2ndcctbss  22514  fgcfil  24340  wilthlem3  26124  cusgrsize2inds  27723  0enwwlksnge1  28130  clwlkclwwlklem2  28265  clwwlknonwwlknonb  28371  conngrv2edg  28460  pjjsi  29963  sltval2  33786  nosupbnd1lem5  33842  dfac21  40807  mogoldbb  45125  nnsum3primesle9  45134  evengpop3  45138  evengpoap3  45139  ztprmneprm  45571  lindslinindsimp1  45686  lindslinindsimp2lem5  45691  flnn0div2ge  45767