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  2407  resf1extb  7935  smogt  8359  inf3lem3  9615  noinfep  9645  cfsmolem  10329  genpnnp  11071  ltaddpr2  11101  fzen  13654  hashge2el2dif  14605  lcmf  16788  ncoprmlnprm  16884  prmgaplem7  17215  initoeu1  18166  termoeu1  18173  dfgrp3lem  19228  cply1mul  22594  scmataddcl  22811  scmatsubcl  22812  2ndcctbss  23754  fgcfil  25572  wilthlem3  27379  ltsval2  27995  nosupbnd1lem5  28051  cusgrsize2inds  30016  0enwwlksnge1  30435  clwlkclwwlklem2  30573  clwwlknonwwlknonb  30679  conngrv2edg  30778  pjjsi  32284  dfac21  44026  mogoldbb  48827  nnsum3primesle9  48836  evengpop3  48840  evengpoap3  48841  ztprmneprm  49403  lindslinindsimp1  49513  lindslinindsimp2lem5  49518  flnn0div2ge  49589