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  2409  resf1extb  7970  smogt  8403  inf3lem3  9658  noinfep  9688  cfsmolem  10375  genpnnp  11117  ltaddpr2  11147  fzen  13701  hashge2el2dif  14652  lcmf  16837  ncoprmlnprm  16933  prmgaplem7  17264  initoeu1  18215  termoeu1  18222  dfgrp3lem  19277  cply1mul  22644  scmataddcl  22861  scmatsubcl  22862  2ndcctbss  23804  fgcfil  25622  wilthlem3  27427  ltsval2  28043  nosupbnd1lem5  28099  cusgrsize2inds  30064  0enwwlksnge1  30483  clwlkclwwlklem2  30621  clwwlknonwwlknonb  30727  conngrv2edg  30826  pjjsi  32332  onprcf1acwevdlem1  36045  dfac21  44261  mogoldbb  49088  nnsum3primesle9  49097  evengpop3  49101  evengpoap3  49102  ztprmneprm  49664  lindslinindsimp1  49774  lindslinindsimp2lem5  49779  flnn0div2ge  49850