MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldc Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 syld.1 . . 3 (𝜑 → (𝜓𝜒))
2 syld.2 . . 3 (𝜑 → (𝜒𝜃))
31, 2syld 47 . 2 (𝜑 → (𝜓𝜃))
43com12 32 1 (𝜓 → (𝜑𝜃))
Colors of variables: wff setvar class
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  2384  wfrlem12  7949  smogt  7987  inf3lem3  9077  noinfep  9107  cfsmolem  9681  genpnnp  10416  ltaddpr2  10446  fzen  12919  hashge2el2dif  13834  lcmf  15967  ncoprmlnprm  16058  prmgaplem7  16383  initoeu1  17263  termoeu1  17270  dfgrp3lem  18189  cply1mul  20923  scmataddcl  21121  scmatsubcl  21122  2ndcctbss  22060  fgcfil  23875  wilthlem3  25655  cusgrsize2inds  27243  0enwwlksnge1  27650  clwlkclwwlklem2  27785  clwwlknonwwlknonb  27891  conngrv2edg  27980  pjjsi  29483  sltval2  33276  nosupbnd1lem5  33325  dfac21  40008  mogoldbb  44301  nnsum3primesle9  44310  evengpop3  44314  evengpoap3  44315  ztprmneprm  44747  lindslinindsimp1  44864  lindslinindsimp2lem5  44869  flnn0div2ge  44945
  Copyright terms: Public domain W3C validator