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  2371  wfrlem12OLD  8340  smogt  8387  inf3lem3  9664  noinfep  9694  cfsmolem  10302  genpnnp  11037  ltaddpr2  11067  fzen  13564  hashge2el2dif  14492  lcmf  16627  ncoprmlnprm  16723  prmgaplem7  17052  initoeu1  18026  termoeu1  18033  dfgrp3lem  19026  cply1mul  22282  scmataddcl  22504  scmatsubcl  22505  2ndcctbss  23445  fgcfil  25285  wilthlem3  27093  sltval2  27681  nosupbnd1lem5  27737  cusgrsize2inds  29385  0enwwlksnge1  29793  clwlkclwwlklem2  29928  clwwlknonwwlknonb  30034  conngrv2edg  30123  pjjsi  31628  dfac21  42762  mogoldbb  47391  nnsum3primesle9  47400  evengpop3  47404  evengpoap3  47405  ztprmneprm  47760  lindslinindsimp1  47874  lindslinindsimp2lem5  47879  flnn0div2ge  47955
  Copyright terms: Public domain W3C validator