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  wfrlem12  8044  smogt  8082  inf3lem3  9223  noinfep  9253  cfsmolem  9849  genpnnp  10584  ltaddpr2  10614  fzen  13094  hashge2el2dif  14011  lcmf  16153  ncoprmlnprm  16247  prmgaplem7  16573  initoeu1  17471  termoeu1  17478  dfgrp3lem  18415  cply1mul  21169  scmataddcl  21367  scmatsubcl  21368  2ndcctbss  22306  fgcfil  24122  wilthlem3  25906  cusgrsize2inds  27495  0enwwlksnge1  27902  clwlkclwwlklem2  28037  clwwlknonwwlknonb  28143  conngrv2edg  28232  pjjsi  29735  sltval2  33545  nosupbnd1lem5  33601  dfac21  40535  mogoldbb  44853  nnsum3primesle9  44862  evengpop3  44866  evengpoap3  44867  ztprmneprm  45299  lindslinindsimp1  45414  lindslinindsimp2lem5  45419  flnn0div2ge  45495