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  8320  smogt  8367  inf3lem3  9625  noinfep  9655  cfsmolem  10265  genpnnp  11000  ltaddpr2  11030  fzen  13518  hashge2el2dif  14441  lcmf  16570  ncoprmlnprm  16664  prmgaplem7  16990  initoeu1  17961  termoeu1  17968  dfgrp3lem  18921  cply1mul  21818  scmataddcl  22018  scmatsubcl  22019  2ndcctbss  22959  fgcfil  24788  wilthlem3  26574  sltval2  27159  nosupbnd1lem5  27215  cusgrsize2inds  28710  0enwwlksnge1  29118  clwlkclwwlklem2  29253  clwwlknonwwlknonb  29359  conngrv2edg  29448  pjjsi  30953  dfac21  41808  mogoldbb  46453  nnsum3primesle9  46462  evengpop3  46466  evengpoap3  46467  ztprmneprm  47023  lindslinindsimp1  47138  lindslinindsimp2lem5  47143  flnn0div2ge  47219