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  3445  ssprsseq  4389  elpr2elpr  4429  disjxiun  4681  oprabid  6717  elovmpt2rab  6922  elovmpt2rab1  6923  mpt2xopoveqd  7392  wfr3g  7458  oewordri  7717  fsuppunbi  8337  r1sdom  8675  pr2ne  8866  kmlem4  9013  kmlem12  9021  domtriomlem  9302  zorn2lem6  9361  axdclem  9379  wunr1om  9579  tskr1om  9627  zindd  11516  hash2pwpr  13296  fi1uzind  13317  swrdccatin2  13533  swrdccatin12  13537  repsdf2  13571  2cshwcshw  13617  cshwcshid  13619  fprodmodd  14772  alzdvds  15089  pwp1fsum  15161  lcmfdvds  15402  prm23ge5  15567  cshwshashlem2  15850  0ringnnzr  19317  01eq0ring  19320  mplcoe5lem  19515  gsummoncoe1  19722  psgndiflemA  19995  gsummatr01lem3  20511  mp2pm2mplem4  20662  fiinopn  20754  cnmptcom  21529  fgcl  21729  fmfnfmlem1  21805  fmco  21812  flffbas  21846  cnpflf2  21851  metcnp3  22392  tngngp3  22507  clmvscom  22936  aalioulem2  24133  ausgrusgrb  26105  usgredg4  26154  nbgr1vtx  26299  nbgrnself2OLD  26304  uhgr0edg0rgrb  26526  wlkres  26623  uhgrwkspth  26707  usgr2wlkspth  26711  uspgrn2crct  26756  crctcshwlkn0  26769  wwlksnredwwlkn  26858  wwlksnextsur  26863  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  frgrnbnb  27273  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  extwwlkfab  27342  cvati  29353  dmdbr5ati  29409  dfon2lem3  31814  frr3g  31904  bj-0int  33180  ptrecube  33539  fzmul  33667  zerdivemp1x  33876  psshepw  38399  ndmaovdistr  41608  ssfz12  41649  fzopredsuc  41658  smonoord  41666  iccpartltu  41686  iccpartgtl  41687  pfxccatin12  41750  lighneallem3  41849  odd2prm2  41952  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbnnsum3prm  42017  elsprel  42050  ringcbasbas  42359  ringcbasbasALTV  42383  ply1mulgsumlem2  42500  ldepsnlinclem1  42619  ldepsnlinclem2  42620  nnolog2flm1  42709  blengt1fldiv2p1  42712
  Copyright terms: Public domain W3C validator