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:  wfrlem12  7583  smogt  7621  inf3lem3  8688  noinfep  8718  cfsmolem  9255  genpnnp  9990  ltaddpr2  10020  fzen  12522  hashge2el2dif  13425  lcmf  15519  ncoprmlnprm  15609  prmgaplem7  15934  initoeu1  16833  termoeu1  16840  dfgrp3lem  17685  cply1mul  19837  scmataddcl  20495  scmatsubcl  20496  2ndcctbss  21431  fgcfil  23240  wilthlem3  24966  cusgrsize2inds  26530  0enwwlksnge1  26944  clwlkclwwlklem2  27094  clwlksfclwwlkOLD  27187  clwwlknonwwlknonb  27225  clwwlknonwwlknonbOLD  27226  conngrv2edg  27318  pjjsi  28839  sltval2  32086  nosupbnd1lem5  32135  wl-dveeq12  33593  dfac21  38107  mogoldbb  42152  nnsum3primesle9  42161  evengpop3  42165  evengpoap3  42166  ztprmneprm  42604  lindslinindsimp1  42725  lindslinindsimp2lem5  42730  flnn0div2ge  42806
  Copyright terms: Public domain W3C validator