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  33  speimfw  1863  axc11nlemOLD2  1975  axc11nlemOLD  2146  axc11nlemALT  2294  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  axc16i  2310  eupickbi  2527  ceqsalgALT  3204  cgsexg  3211  cgsex2g  3212  cgsex4g  3213  spc2egv  3268  spc3egv  3270  disjne  3974  uneqdifeq  4009  uneqdifeqOLD  4010  relresfld  5565  unixpid  5573  ordnbtwn  5719  sucssel  5722  ordelinel  5728  fvimacnv  6225  ordsuc  6884  tfi  6923  fornex  7006  f1ovv  7008  wfrlem4  7283  wfrlem10  7289  tz7.49  7405  oeworde  7538  undifixp  7808  dom2d  7860  findcard  8062  fisupg  8071  dffi3  8198  fiinfg  8266  noinfep  8418  cantnflem2  8448  tcmin  8478  rankr1ag  8526  rankelb  8548  rankunb  8574  rankxpsuc  8606  alephordi  8758  alephsucdom  8763  alephinit  8779  dfac9  8819  ackbij2lem4  8925  cff1  8941  cfslbn  8950  cfcoflem  8955  cfcof  8957  infpssrlem5  8990  isfin7-2  9079  acncc  9123  domtriomlem  9125  axdc3lem2  9134  ttukeylem1  9192  iundom2g  9219  axpowndlem3  9278  wunex2  9417  grupr  9476  gruiun  9478  eltskm  9522  nqereu  9608  addcanpr  9725  axpre-sup  9847  relin01  10404  nneo  11296  zeo2  11299  xrub  11973  uznfz  12250  difelfzle  12279  ssfzo12  12385  facndiv  12895  hashf1rnOLD  12960  hashgt12el2  13026  hash2prde  13064  hash2pwpr  13068  fi1uzind  13083  fi1uzindOLD  13089  swrdswrd  13261  swrdccatin2  13287  swrdccatin12lem2  13289  swrdccatin12  13291  swrdccat3  13292  swrdccatid  13297  repswswrd  13331  2cshwcshw  13371  relexpcnvd  13573  relexpdmd  13581  relexprnd  13585  relexpfldd  13587  relexpaddd  13591  fsumcom2  14296  fsumcom2OLD  14297  fprodss  14466  fprodcom2  14502  fprodcom2OLD  14503  sumodd  14898  ndvdssub  14920  eucalglt  15085  prmind2  15185  coprm  15210  prmdiveq  15278  prmdvdsprmop  15534  prmgaplem5  15546  drsdir  16707  lublecllem  16760  istos  16807  tsrlin  16991  dirge  17009  mhmlin  17114  issubg2  17381  nsgbi  17397  symgextf1lem  17612  sylow2a  17806  issubrg2  18572  abvmul  18601  abvtri  18602  lmodlema  18640  lspsnel6  18764  lmhmlin  18805  lbsind  18850  0ring01eq  19041  01eq0ring  19042  gsummoncoe1  19444  ipcj  19746  obsip  19832  lindsss  19930  mamufacex  19962  mavmulsolcl  20124  slesolvec  20252  inopn  20477  basis1  20513  tgss  20531  tgcl  20532  elcls3  20645  neindisj2  20685  cncls  20836  1stcelcls  21022  qtoptop2  21260  nrmr0reg  21310  fbasssin  21398  fbfinnfr  21403  fbunfip  21431  filufint  21482  uffix  21483  ufinffr  21491  ufilen  21492  fmfnfmlem1  21516  flftg  21558  alexsubALT  21613  xmeteq0  21901  blssexps  21989  blssex  21990  mopni3  22057  neibl  22064  metss  22071  metcnp3  22103  nmvs  22238  reperflem  22377  iccntr  22380  reconnlem2  22386  lebnumlem3  22518  caubl  22859  bcthlem5  22878  ovolunlem1  23017  voliunlem1  23070  volsuplem  23075  ellimc3  23394  lhop1lem  23525  ulmss  23900  2lgsoddprmlem3  24884  dchrisumlema  24922  usgrarnedg  25707  usgrafisbase  25737  uvtxisvtx  25812  wlkn0  25849  usgrwlknloop  25887  usgra2wlkspthlem1  25941  usgrcyclnl2  25963  wlk0  26083  clwwlknprop  26094  clwlkisclwwlklem0  26110  wwlkext2clwwlk  26125  clwlkfclwwlk  26165  usgfiregdegfi  26232  eupatrl  26289  2pthfrgra  26332  3cyclfrgrarn2  26335  frgrancvvdeqlemB  26359  frgrawopreg1  26371  frgrawopreg2  26372  frgraeu  26375  numclwwlkovf2ex  26407  frgraregord013  26439  frgraogt3nreg  26441  ablocom  26580  ubthlem1  26904  shaddcl  27252  shmulcl  27253  spansnss2  27612  cnopc  27950  cnfnc  27967  adj1  27970  pjorthcoi  28206  stj  28272  mdsl1i  28358  chirredlem1  28427  mdsymlem5  28444  cdj3lem2b  28474  slmdlema  28881  pconcn  30254  cvmlift2lem1  30332  ss2mcls  30513  dfon2lem6  30731  frrlem4  30821  nofv  30848  nodenselem4  30877  nn0prpw  31282  waj-ax  31377  lukshef-ax2  31378  bj-alrim  31664  bj-nexdt  31668  sucneqond  32183  ptrecube  32373  poimirlem26  32399  poimirlem29  32402  heiborlem1  32574  rngodm1dm2  32695  rngoueqz  32703  zerdivemp1x  32710  isdrngo3  32722  0rngo  32790  pridl  32800  ispridlc  32833  isdmn3  32837  dmnnzd  32838  lshpcmp  33087  omllaw  33342  dochexmidlem7  35567  lspindp5  35871  dfac21  36448  eexinst11  37548  ax6e2eq  37588  e222  37676  e111  37714  eel12131  37753  e333  37775  iccpartigtl  39756  iccpartgt  39760  lighneallem3  39857  lighneal  39861  bgoldbtbndlem2  40017  pfxccatin12lem2  40082  pfxccatin12  40083  pfxccat3  40084  2f1fvneq  40128  imarnf1pr  40132  2ffzoeq  40178  umgrnloopv  40323  usgrnloopvALT  40420  umgrres1lem  40521  upgrres1  40524  nbuhgr  40557  cplgrop  40651  fusgrregdegfi  40761  g01wlk0  40852  1wlkdlem2  40884  upgrwlkdvdelem  40934  crctcsh1wlkn0lem4  41008  crctcsh1wlkn0lem5  41009  umgrwwlks2on  41153  elwspths2spth  41163  clwlkclwwlklem2a  41199  clwlkclwwlklem3  41202  clwlksfclwwlk  41261  3cyclfrgrrn2  41449  frgrncvvdeqlemB  41469  frgrwopreg1  41479  frgrwopreg2  41480  frgreu  41483  av-numclwwlkovf2ex  41509  av-frgraregord013  41541  av-frgraogt3nreg  41543  nrhmzr  41655  nzerooringczr  41856  gsumpr  41924  lincdifsn  41999  snlindsntor  42046  lincresunit3lem1  42054  lincresunit3lem2  42055  lincresunit3  42056
  Copyright terms: Public domain W3C validator