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  2386  wfrlem12  7955  smogt  7993  inf3lem3  9081  noinfep  9111  cfsmolem  9680  genpnnp  10415  ltaddpr2  10445  fzen  12912  hashge2el2dif  13826  lcmf  15965  ncoprmlnprm  16056  prmgaplem7  16381  initoeu1  17259  termoeu1  17266  dfgrp3lem  18135  cply1mul  20390  scmataddcl  21053  scmatsubcl  21054  2ndcctbss  21991  fgcfil  23801  wilthlem3  25574  cusgrsize2inds  27162  0enwwlksnge1  27569  clwlkclwwlklem2  27705  clwwlknonwwlknonb  27812  conngrv2edg  27901  pjjsi  29404  sltval2  33060  nosupbnd1lem5  33109  dfac21  39544  mogoldbb  43827  nnsum3primesle9  43836  evengpop3  43840  evengpoap3  43841  ztprmneprm  44323  lindslinindsimp1  44440  lindslinindsimp2lem5  44445  flnn0div2ge  44521
  Copyright terms: Public domain W3C validator