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  2381  resf1extb  7957  wfrlem12OLD  8361  smogt  8408  inf3lem3  9671  noinfep  9701  cfsmolem  10311  genpnnp  11046  ltaddpr2  11076  fzen  13582  hashge2el2dif  14520  lcmf  16671  ncoprmlnprm  16766  prmgaplem7  17096  initoeu1  18057  termoeu1  18064  dfgrp3lem  19057  cply1mul  22301  scmataddcl  22523  scmatsubcl  22524  2ndcctbss  23464  fgcfil  25306  wilthlem3  27114  sltval2  27702  nosupbnd1lem5  27758  cusgrsize2inds  29472  0enwwlksnge1  29885  clwlkclwwlklem2  30020  clwwlknonwwlknonb  30126  conngrv2edg  30215  pjjsi  31720  dfac21  43083  mogoldbb  47777  nnsum3primesle9  47786  evengpop3  47790  evengpoap3  47791  ztprmneprm  48268  lindslinindsimp1  48379  lindslinindsimp2lem5  48384  flnn0div2ge  48459
  Copyright terms: Public domain W3C validator