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  1966  sbequ2OLD  2250  axc16i  2450  eupickbi  2701  ceqsalgALT  3480  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spcegv  3548  spc2egv  3551  disjne  4365  uneqdifeq  4399  preqsnd  4752  preq12nebg  4756  opthprneg  4758  relresfld  6099  unixpid  6107  ordnbtwn  6253  sucssel  6255  ordelinel  6261  fvimacnv  6804  2f1fvneq  7000  ordsuc  7513  tfi  7552  fornex  7643  f1ovv  7645  opreuopreu  7720  wfrlem4  7945  wfrlem10  7951  tz7.49  8068  oeworde  8206  dom2d  8537  findcard  8745  fisupg  8754  dffi3  8883  noinfep  9111  cantnflem2  9141  tcmin  9171  rankr1ag  9219  rankunb  9267  rankxpsuc  9299  alephordi  9489  alephsucdom  9494  alephinit  9510  dfac9  9551  ackbij2lem4  9657  cff1  9673  cfslbn  9682  cfcoflem  9687  cfcof  9689  infpssrlem5  9722  isfin7-2  9811  acncc  9855  domtriomlem  9857  axdc3lem2  9866  ttukeylem1  9924  iundom2g  9955  axpowndlem3  10014  wunex2  10153  grupr  10212  gruiun  10214  eltskm  10258  nqereu  10344  addcanpr  10461  axpre-sup  10584  relin01  11157  nneo  12058  zeo2  12061  xrub  12697  uznfz  12989  difelfzle  13019  ssfzo12  13129  facndiv  13648  hashgt12el2  13784  hash2prde  13828  hash2pwpr  13834  hashle2prv  13836  fi1uzind  13855  swrdswrd  14062  pfxccatin12lem2  14088  pfxccatin12  14090  pfxccat3  14091  cshwidxmod  14160  2cshwcshw  14182  fsumcom2  15125  fprodss  15298  fprodcom2  15334  sumodd  15733  ndvdssub  15754  eucalglt  15923  prmind2  16023  coprm  16049  prmdiveq  16117  prmdvdsprmop  16373  prmgaplem5  16385  cicsym  17070  drsdir  17541  lublecllem  17594  istos  17641  tsrlin  17825  dirge  17843  mhmlin  17959  issubg2  18290  nsgbi  18305  symgextf1lem  18544  sylow2a  18740  gsumpr  19072  issubrg2  19552  abvmul  19597  abvtri  19598  lmodlema  19636  rmodislmodlem  19698  rmodislmod  19699  lspsnel6  19763  lmhmlin  19804  lbsind  19849  0ringnnzr  20039  0ring01eq  20041  01eq0ring  20042  ipcj  20327  obsip  20414  lindsss  20517  mamufacex  21000  mavmulsolcl  21160  slesolvec  21288  inopn  21508  basis1  21559  tgss  21577  tgcl  21578  elcls3  21692  neindisj2  21732  cncls  21883  1stcelcls  22070  qtoptop2  22308  nrmr0reg  22358  fbasssin  22445  fbfinnfr  22450  fbunfip  22478  filufint  22529  uffix  22530  ufinffr  22538  ufilen  22539  fmfnfmlem1  22563  flftg  22605  alexsubALT  22660  xmeteq0  22949  blssexps  23037  blssex  23038  mopni3  23105  neibl  23112  metss  23119  metcnp3  23151  nmvs  23286  iccntr  23430  reconnlem2  23436  lebnumlem3  23572  caubl  23916  bcthlem5  23936  ovolunlem1  24105  voliunlem1  24158  volsuplem  24163  ellimc3  24486  logbgcd1irr  25384  lgsqrmodndvds  25941  gausslemma2dlem0i  25952  2lgsoddprmlem3  26002  dchrisumlema  26076  umgrnloopv  26903  usgrnloopvALT  26995  umgrres1lem  27104  upgrres1  27107  nbuhgr  27137  cplgrop  27231  fusgrregdegfi  27363  g0wlk0  27445  wlkdlem2  27477  upgrwlkdvdelem  27529  crctcshwlkn0lem3  27602  crctcshwlkn0lem5  27604  wspn0  27714  umgrwwlks2on  27747  elwspths2spth  27757  clwlkclwwlklem2a  27787  clwlkclwwlklem3  27790  clwwlkn1loopb  27832  clwwlknonwwlknonb  27895  clwwlknonex2lem2  27897  3cyclfrgrrn2  28076  frgrncvvdeqlem8  28095  frgrwopregasn  28105  frgrwopregbsn  28106  frgrwopreg1  28107  frgrwopreg2  28108  frgrregord013  28184  frgrogt3nreg  28186  ablocom  28335  ubthlem1  28657  shaddcl  29004  shmulcl  29005  spansnss2  29362  cnopc  29700  cnfnc  29717  adj1  29720  pjorthcoi  29956  stj  30022  mdsl1i  30108  chirredlem1  30177  mdsymlem5  30194  cdj3lem2b  30224  slmdlema  30885  isprmidlc  31035  pconncn  32585  cvmlift2lem1  32663  fmla0xp  32744  ss2mcls  32929  dfon2lem6  33147  frrlem4  33240  nofv  33278  nolesgn2o  33292  nosupbnd1lem5  33326  waj-ax  33876  lukshef-ax2  33877  bj-alrim  34141  bj-nexdt  34145  sucneqond  34783  rdgssun  34796  ptrecube  35056  poimirlem26  35082  poimirlem29  35085  heiborlem1  35248  rngodm1dm2  35369  rngoueqz  35377  zerdivemp1x  35384  isdrngo3  35396  0rngo  35464  pridl  35474  ispridlc  35507  isdmn3  35511  dmnnzd  35512  elrelscnveq3  35890  lshpcmp  36283  omllaw  36538  dochexmidlem7  38761  lspindp5  39065  fsuppind  39453  dfac21  40007  eexinst11  41230  ax6e2eq  41260  e222  41339  e111  41377  e333  41436  imarnf1pr  43835  2ffzoeq  43882  iccpartigtl  43937  iccpartgt  43941  lighneallem3  44122  lighneal  44126  requad1  44137  evenltle  44232  fppr2odd  44246  sgoldbeven3prm  44298  bgoldbtbndlem2  44321  isomuspgrlem2b  44344  nrhmzr  44494  nzerooringczr  44693  lincdifsn  44830  lindslinindimp2lem4  44867  snlindsntor  44877  lincresunit3lem1  44885  lincresunit3lem2  44886  setrec1lem2  45215
  Copyright terms: Public domain W3C validator