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

Theorem syl5com 31
Description: Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.)
Hypotheses
Ref Expression
syl5com.1 (𝜑𝜓)
syl5com.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5com (𝜑 → (𝜒𝜃))

Proof of Theorem syl5com
StepHypRef Expression
1 syl5com.1 . . 3 (𝜑𝜓)
21a1d 25 . 2 (𝜑 → (𝜒𝜓))
3 syl5com.2 . 2 (𝜒 → (𝜓𝜃))
42, 3sylcom 30 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:  com12  32  syl5  34  speimfw  1957  sbequ2OLD  2241  axc16i  2450  eupickbi  2714  ceqsalgALT  3528  cgsexg  3535  cgsex2g  3536  cgsex4g  3537  spcegv  3594  spc2egv  3597  disjne  4400  uneqdifeq  4434  preqsnd  4781  preq12nebg  4785  opthprneg  4787  relresfld  6120  unixpid  6128  ordnbtwn  6274  sucssel  6276  ordelinel  6282  fvimacnv  6815  2f1fvneq  7009  ordsuc  7518  tfi  7557  fornex  7646  f1ovv  7648  opreuopreu  7723  wfrlem4  7947  wfrlem10  7953  tz7.49  8070  oeworde  8208  dom2d  8538  findcard  8745  fisupg  8754  dffi3  8883  noinfep  9111  cantnflem2  9141  tcmin  9171  rankr1ag  9219  rankunb  9267  rankxpsuc  9299  alephordi  9488  alephsucdom  9493  alephinit  9509  dfac9  9550  ackbij2lem4  9652  cff1  9668  cfslbn  9677  cfcoflem  9682  cfcof  9684  infpssrlem5  9717  isfin7-2  9806  acncc  9850  domtriomlem  9852  axdc3lem2  9861  ttukeylem1  9919  iundom2g  9950  axpowndlem3  10009  wunex2  10148  grupr  10207  gruiun  10209  eltskm  10253  nqereu  10339  addcanpr  10456  axpre-sup  10579  relin01  11152  nneo  12054  zeo2  12057  xrub  12693  uznfz  12978  difelfzle  13008  ssfzo12  13118  facndiv  13636  hashgt12el2  13772  hash2prde  13816  hash2pwpr  13822  hashle2prv  13824  fi1uzind  13843  swrdswrd  14055  pfxccatin12lem2  14081  pfxccatin12  14083  pfxccat3  14084  cshwidxmod  14153  2cshwcshw  14175  relexpcnvd  14383  relexpdmd  14391  relexprnd  14395  relexpfldd  14397  relexpaddd  14401  fsumcom2  15117  fprodss  15290  fprodcom2  15326  sumodd  15727  ndvdssub  15748  eucalglt  15917  prmind2  16017  coprm  16043  prmdiveq  16111  prmdvdsprmop  16367  prmgaplem5  16379  cicsym  17062  drsdir  17533  lublecllem  17586  istos  17633  tsrlin  17817  dirge  17835  mhmlin  17951  issubg2  18232  nsgbi  18247  symgextf1lem  18477  sylow2a  18673  gsumpr  19004  issubrg2  19484  abvmul  19529  abvtri  19530  lmodlema  19568  rmodislmodlem  19630  rmodislmod  19631  lspsnel6  19695  lmhmlin  19736  lbsind  19781  0ringnnzr  19970  0ring01eq  19972  01eq0ring  19973  ipcj  20706  obsip  20793  lindsss  20896  mamufacex  20928  mavmulsolcl  21088  slesolvec  21216  inopn  21435  basis1  21486  tgss  21504  tgcl  21505  elcls3  21619  neindisj2  21659  cncls  21810  1stcelcls  21997  qtoptop2  22235  nrmr0reg  22285  fbasssin  22372  fbfinnfr  22377  fbunfip  22405  filufint  22456  uffix  22457  ufinffr  22465  ufilen  22466  fmfnfmlem1  22490  flftg  22532  alexsubALT  22587  xmeteq0  22875  blssexps  22963  blssex  22964  mopni3  23031  neibl  23038  metss  23045  metcnp3  23077  nmvs  23212  iccntr  23356  reconnlem2  23362  lebnumlem3  23494  caubl  23838  bcthlem5  23858  ovolunlem1  24025  voliunlem1  24078  volsuplem  24083  ellimc3  24404  logbgcd1irr  25299  lgsqrmodndvds  25856  gausslemma2dlem0i  25867  2lgsoddprmlem3  25917  dchrisumlema  25991  umgrnloopv  26818  usgrnloopvALT  26910  umgrres1lem  27019  upgrres1  27022  nbuhgr  27052  cplgrop  27146  fusgrregdegfi  27278  g0wlk0  27360  wlkdlem2  27392  upgrwlkdvdelem  27444  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  wspn0  27630  umgrwwlks2on  27663  elwspths2spth  27673  clwlkclwwlklem2a  27703  clwlkclwwlklem3  27706  clwwlkn1loopb  27748  clwwlknonwwlknonb  27812  clwwlknonex2lem2  27814  3cyclfrgrrn2  27993  frgrncvvdeqlem8  28012  frgrwopregasn  28022  frgrwopregbsn  28023  frgrwopreg1  28024  frgrwopreg2  28025  frgrregord013  28101  frgrogt3nreg  28103  ablocom  28252  ubthlem1  28574  shaddcl  28921  shmulcl  28922  spansnss2  29279  cnopc  29617  cnfnc  29634  adj1  29637  pjorthcoi  29873  stj  29939  mdsl1i  30025  chirredlem1  30094  mdsymlem5  30111  cdj3lem2b  30141  slmdlema  30758  isprmidlc  30881  pconncn  32368  cvmlift2lem1  32446  fmla0xp  32527  ss2mcls  32712  dfon2lem6  32930  frrlem4  33023  nofv  33061  nolesgn2o  33075  nosupbnd1lem5  33109  waj-ax  33659  lukshef-ax2  33660  bj-alrim  33924  bj-nexdt  33928  sucneqond  34528  rdgssun  34541  ptrecube  34773  poimirlem26  34799  poimirlem29  34802  heiborlem1  34970  rngodm1dm2  35091  rngoueqz  35099  zerdivemp1x  35106  isdrngo3  35118  0rngo  35186  pridl  35196  ispridlc  35229  isdmn3  35233  dmnnzd  35234  elrelscnveq3  35611  lshpcmp  36004  omllaw  36259  dochexmidlem7  38482  lspindp5  38786  dfac21  39544  eexinst11  40738  ax6e2eq  40768  e222  40847  e111  40885  e333  40944  imarnf1pr  43358  2ffzoeq  43405  iccpartigtl  43460  iccpartgt  43464  lighneallem3  43649  lighneal  43653  requad1  43664  evenltle  43759  fppr2odd  43773  sgoldbeven3prm  43825  bgoldbtbndlem2  43848  isomuspgrlem2b  43871  nrhmzr  44072  nzerooringczr  44271  lincdifsn  44407  lindslinindimp2lem4  44444  snlindsntor  44454  lincresunit3lem1  44462  lincresunit3lem2  44463  setrec1lem2  44719
  Copyright terms: Public domain W3C validator