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  5579  unixpid  5587  ordnbtwn  5733  sucssel  5736  ordelinel  5742  fvimacnv  6240  ordsuc  6906  tfi  6945  fornex  7028  f1ovv  7030  wfrlem4  7305  wfrlem10  7311  tz7.49  7427  oeworde  7560  undifixp  7830  dom2d  7882  findcard  8084  fisupg  8093  dffi3  8220  fiinfg  8288  noinfep  8440  cantnflem2  8470  tcmin  8500  rankr1ag  8548  rankelb  8570  rankunb  8596  rankxpsuc  8628  alephordi  8780  alephsucdom  8785  alephinit  8801  dfac9  8841  ackbij2lem4  8947  cff1  8963  cfslbn  8972  cfcoflem  8977  cfcof  8979  infpssrlem5  9012  isfin7-2  9101  acncc  9145  domtriomlem  9147  axdc3lem2  9156  ttukeylem1  9214  iundom2g  9241  axpowndlem3  9300  wunex2  9439  grupr  9498  gruiun  9500  eltskm  9544  nqereu  9630  addcanpr  9747  axpre-sup  9869  relin01  10431  nneo  11337  zeo2  11340  xrub  12014  uznfz  12292  difelfzle  12321  ssfzo12  12427  facndiv  12937  hashf1rnOLD  13005  hashgt12el2  13071  hash2prde  13109  hash2pwpr  13115  fi1uzind  13134  fi1uzindOLD  13140  swrdswrd  13312  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12  13342  swrdccat3  13343  swrdccatid  13348  repswswrd  13382  2cshwcshw  13422  relexpcnvd  13624  relexpdmd  13632  relexprnd  13636  relexpfldd  13638  relexpaddd  13642  fsumcom2  14347  fsumcom2OLD  14348  fprodss  14517  fprodcom2  14553  fprodcom2OLD  14554  sumodd  14949  ndvdssub  14971  eucalglt  15136  prmind2  15236  coprm  15261  prmdiveq  15329  prmdvdsprmop  15585  prmgaplem5  15597  drsdir  16758  lublecllem  16811  istos  16858  tsrlin  17042  dirge  17060  mhmlin  17165  issubg2  17432  nsgbi  17448  symgextf1lem  17663  sylow2a  17857  issubrg2  18623  abvmul  18652  abvtri  18653  lmodlema  18691  lspsnel6  18815  lmhmlin  18856  lbsind  18901  0ring01eq  19092  01eq0ring  19093  gsummoncoe1  19495  ipcj  19798  obsip  19884  lindsss  19982  mamufacex  20014  mavmulsolcl  20176  slesolvec  20304  inopn  20529  basis1  20565  tgss  20583  tgcl  20584  elcls3  20697  neindisj2  20737  cncls  20888  1stcelcls  21074  qtoptop2  21312  nrmr0reg  21362  fbasssin  21450  fbfinnfr  21455  fbunfip  21483  filufint  21534  uffix  21535  ufinffr  21543  ufilen  21544  fmfnfmlem1  21568  flftg  21610  alexsubALT  21665  xmeteq0  21953  blssexps  22041  blssex  22042  mopni3  22109  neibl  22116  metss  22123  metcnp3  22155  nmvs  22290  reperflem  22429  iccntr  22432  reconnlem2  22438  lebnumlem3  22570  caubl  22914  bcthlem5  22933  ovolunlem1  23072  voliunlem1  23125  volsuplem  23130  ellimc3  23449  lhop1lem  23580  ulmss  23955  2lgsoddprmlem3  24939  dchrisumlema  24977  umgrnloopv  25772  usgrarnedg  25913  usgrafisbase  25943  uvtxisvtx  26018  wlkn0  26055  usgrwlknloop  26093  usgra2wlkspthlem1  26147  usgrcyclnl2  26169  wlk0  26289  clwwlknprop  26300  clwlkisclwwlklem0  26316  wwlkext2clwwlk  26331  clwlkfclwwlk  26371  usgfiregdegfi  26438  eupatrl  26495  2pthfrgra  26538  3cyclfrgrarn2  26541  frgrancvvdeqlemB  26565  frgrawopreg1  26577  frgrawopreg2  26578  frgraeu  26581  numclwwlkovf2ex  26613  frgraregord013  26645  frgraogt3nreg  26647  ablocom  26786  ubthlem1  27110  shaddcl  27458  shmulcl  27459  spansnss2  27818  cnopc  28156  cnfnc  28173  adj1  28176  pjorthcoi  28412  stj  28478  mdsl1i  28564  chirredlem1  28633  mdsymlem5  28650  cdj3lem2b  28680  slmdlema  29087  pconcn  30460  cvmlift2lem1  30538  ss2mcls  30719  dfon2lem6  30937  frrlem4  31027  nofv  31054  nodenselem4  31083  nn0prpw  31488  waj-ax  31583  lukshef-ax2  31584  bj-alrim  31870  bj-nexdt  31874  sucneqond  32389  ptrecube  32579  poimirlem26  32605  poimirlem29  32608  heiborlem1  32780  rngodm1dm2  32901  rngoueqz  32909  zerdivemp1x  32916  isdrngo3  32928  0rngo  32996  pridl  33006  ispridlc  33039  isdmn3  33043  dmnnzd  33044  lshpcmp  33293  omllaw  33548  dochexmidlem7  35773  lspindp5  36077  dfac21  36654  eexinst11  37754  ax6e2eq  37794  e222  37882  e111  37920  eel12131  37959  e333  37981  iccpartigtl  39961  iccpartgt  39965  lighneallem3  40062  lighneal  40066  bgoldbtbndlem2  40222  pfxccatin12lem2  40287  pfxccatin12  40288  pfxccat3  40289  2f1fvneq  40322  imarnf1pr  40326  2ffzoeq  40361  usgrnloopvALT  40428  umgrres1lem  40529  upgrres1  40532  nbuhgr  40565  cplgrop  40659  fusgrregdegfi  40769  g01wlk0  40860  1wlkdlem2  40892  upgrwlkdvdelem  40942  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  umgrwwlks2on  41161  elwspths2spth  41171  clwlkclwwlklem2a  41207  clwlkclwwlklem3  41210  clwlksfclwwlk  41269  3cyclfrgrrn2  41457  frgrncvvdeqlemB  41477  frgrwopreg1  41487  frgrwopreg2  41488  frgreu  41491  av-numclwwlkovf2ex  41517  av-frgraregord013  41549  av-frgraogt3nreg  41551  nrhmzr  41663  nzerooringczr  41864  gsumpr  41932  lincdifsn  42007  snlindsntor  42054  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064  setrec1lem2  42234
  Copyright terms: Public domain W3C validator