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  2375  wfrlem12OLD  8265  smogt  8312  inf3lem3  9565  noinfep  9595  cfsmolem  10205  genpnnp  10940  ltaddpr2  10970  fzen  13457  hashge2el2dif  14378  lcmf  16508  ncoprmlnprm  16602  prmgaplem7  16928  initoeu1  17896  termoeu1  17903  dfgrp3lem  18843  cply1mul  21663  scmataddcl  21863  scmatsubcl  21864  2ndcctbss  22804  fgcfil  24633  wilthlem3  26417  sltval2  27002  nosupbnd1lem5  27058  cusgrsize2inds  28399  0enwwlksnge1  28807  clwlkclwwlklem2  28942  clwwlknonwwlknonb  29048  conngrv2edg  29137  pjjsi  30640  dfac21  41371  mogoldbb  45949  nnsum3primesle9  45958  evengpop3  45962  evengpoap3  45963  ztprmneprm  46395  lindslinindsimp1  46510  lindslinindsimp2lem5  46515  flnn0div2ge  46591
  Copyright terms: Public domain W3C validator