MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl11 Structured version   Visualization version   GIF version

Theorem syl11 33
Description: A syllogism inference. Commuted form of an instance of syl 17. (Contributed by BJ, 25-Oct-2021.)
Hypotheses
Ref Expression
syl11.1 (𝜑 → (𝜓𝜒))
syl11.2 (𝜃𝜑)
Assertion
Ref Expression
syl11 (𝜓 → (𝜃𝜒))

Proof of Theorem syl11
StepHypRef Expression
1 syl11.2 . . 3 (𝜃𝜑)
2 syl11.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl 17 . 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:  pm2.86i  109  2rmorex  3406  ssprsseq  4348  elpr2elpr  4389  disjxiun  4640  oprabid  6662  elovmpt2rab  6865  elovmpt2rab1  6866  mpt2xopoveqd  7332  wfr3g  7398  oewordri  7657  fsuppunbi  8281  r1sdom  8622  pr2ne  8813  kmlem4  8960  kmlem12  8968  domtriomlem  9249  zorn2lem6  9308  axdclem  9326  wunr1om  9526  tskr1om  9574  zindd  11463  hash2pwpr  13241  fi1uzind  13262  swrdccatin2  13468  swrdccatin12  13472  repsdf2  13506  2cshwcshw  13552  cshwcshid  13554  fprodmodd  14709  alzdvds  15023  pwp1fsum  15095  lcmfdvds  15336  prm23ge5  15501  cshwshashlem2  15784  0ringnnzr  19250  01eq0ring  19253  mplcoe5lem  19448  gsummoncoe1  19655  psgndiflemA  19928  gsummatr01lem3  20444  mp2pm2mplem4  20595  fiinopn  20687  cnmptcom  21462  fgcl  21663  fmfnfmlem1  21739  fmco  21746  flffbas  21780  cnpflf2  21785  metcnp3  22326  tngngp3  22441  clmvscom  22871  aalioulem2  24069  ausgrusgrb  26041  usgredg4  26090  nbgr1vtx  26235  nbgrnself2  26240  uhgr0edg0rgrb  26451  wlkres  26548  uhgrwkspth  26632  usgr2wlkspth  26636  uspgrn2crct  26681  crctcshwlkn0  26694  wwlksnredwwlkn  26771  wwlksnextsur  26776  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  frgrnbnb  27137  extwwlkfablem2  27184  extwwlkfab  27194  cvati  29195  dmdbr5ati  29251  dfon2lem3  31664  frr3g  31753  bj-0int  33030  ptrecube  33380  fzmul  33508  zerdivemp1x  33717  psshepw  37902  ndmaovdistr  41050  ssfz12  41087  fzopredsuc  41096  smonoord  41105  iccpartltu  41125  iccpartgtl  41126  pfxccatin12  41190  lighneallem3  41289  odd2prm2  41392  nnsum4primeseven  41453  nnsum4primesevenALTV  41454  bgoldbnnsum3prm  41457  elsprel  41490  ringcbasbas  41799  ringcbasbasALTV  41823  ply1mulgsumlem2  41940  ldepsnlinclem1  42059  ldepsnlinclem2  42060  nnolog2flm1  42149  blengt1fldiv2p1  42152
  Copyright terms: Public domain W3C validator