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  1933  axc11nOLD  2343  axc16i  2353  eupickbi  2568  ceqsalgALT  3262  cgsexg  3269  cgsex2g  3270  cgsex4g  3271  spc2egv  3326  spc3egv  3328  disjne  4055  uneqdifeq  4090  uneqdifeqOLD  4091  relresfld  5700  unixpid  5708  ordnbtwn  5854  sucssel  5857  ordelinel  5863  fvimacnv  6372  2f1fvneq  6557  ordsuc  7056  tfi  7095  fornex  7177  f1ovv  7179  wfrlem4  7463  wfrlem10  7469  tz7.49  7585  oeworde  7718  dom2d  8038  findcard  8240  fisupg  8249  dffi3  8378  fiinfg  8446  noinfep  8595  cantnflem2  8625  tcmin  8655  rankr1ag  8703  rankelb  8725  rankunb  8751  rankxpsuc  8783  alephordi  8935  alephsucdom  8940  alephinit  8956  dfac9  8996  ackbij2lem4  9102  cff1  9118  cfslbn  9127  cfcoflem  9132  cfcof  9134  infpssrlem5  9167  isfin7-2  9256  acncc  9300  domtriomlem  9302  axdc3lem2  9311  ttukeylem1  9369  iundom2g  9400  axpowndlem3  9459  wunex2  9598  grupr  9657  gruiun  9659  eltskm  9703  nqereu  9789  addcanpr  9906  axpre-sup  10028  relin01  10590  nneo  11499  zeo2  11502  xrub  12180  uznfz  12461  difelfzle  12491  ssfzo12  12601  facndiv  13115  hashgt12el2  13249  hash2prde  13290  hash2pwpr  13296  hashle2prv  13298  fi1uzind  13317  swrdswrd  13506  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12  13537  swrdccat3  13538  swrdccatid  13543  repswswrd  13577  2cshwcshw  13617  relexpcnvd  13820  relexpdmd  13828  relexprnd  13832  relexpfldd  13834  relexpaddd  13838  fsumcom2  14549  fsumcom2OLD  14550  fprodss  14722  fprodcom2  14758  fprodcom2OLD  14759  sumodd  15158  ndvdssub  15180  eucalglt  15345  prmind2  15445  coprm  15470  prmdiveq  15538  prmdvdsprmop  15794  prmgaplem5  15806  drsdir  16982  lublecllem  17035  istos  17082  tsrlin  17266  dirge  17284  mhmlin  17389  issubg2  17656  nsgbi  17672  symgextf1lem  17886  sylow2a  18080  issubrg2  18848  abvmul  18877  abvtri  18878  lmodlema  18916  rmodislmodlem  18978  rmodislmod  18979  lspsnel6  19042  lmhmlin  19083  lbsind  19128  0ring01eq  19319  01eq0ring  19320  gsummoncoe1  19722  ipcj  20027  obsip  20113  lindsss  20211  mamufacex  20243  mavmulsolcl  20405  slesolvec  20533  inopn  20752  basis1  20802  tgss  20820  tgcl  20821  elcls3  20935  neindisj2  20975  cncls  21126  1stcelcls  21312  qtoptop2  21550  nrmr0reg  21600  fbasssin  21687  fbfinnfr  21692  fbunfip  21720  filufint  21771  uffix  21772  ufinffr  21780  ufilen  21781  fmfnfmlem1  21805  flftg  21847  alexsubALT  21902  xmeteq0  22190  blssexps  22278  blssex  22279  mopni3  22346  neibl  22353  metss  22360  metcnp3  22392  nmvs  22527  reperflem  22668  iccntr  22671  reconnlem2  22677  lebnumlem3  22809  caubl  23152  bcthlem5  23171  ovolunlem1  23311  voliunlem1  23364  volsuplem  23369  ellimc3  23688  lhop1lem  23821  ulmss  24196  lgsqrmodndvds  25123  2lgsoddprmlem3  25184  dchrisumlema  25222  umgrnloopv  26046  usgrnloopvALT  26138  umgrres1lem  26247  upgrres1  26250  nbuhgr  26284  cplgrop  26389  fusgrregdegfi  26521  g0wlk0  26604  wlkdlem2  26636  upgrwlkdvdelem  26688  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  wspn0  26889  umgrwwlks2on  26923  elwspths2spth  26934  clwlkclwwlklem2a  26964  clwlkclwwlklem3  26967  clwwlkn1loopb  27006  clwlksfclwwlk  27049  clwwlknonex2lem2  27083  3cyclfrgrrn2  27267  frgrncvvdeqlem8  27286  frgrwopregasn  27296  frgrwopregbsn  27297  frgrwopreg1  27298  frgrwopreg2  27299  frgrregord013  27382  frgrogt3nreg  27384  ablocom  27530  ubthlem1  27854  shaddcl  28202  shmulcl  28203  spansnss2  28562  cnopc  28900  cnfnc  28917  adj1  28920  pjorthcoi  29156  stj  29222  mdsl1i  29308  chirredlem1  29377  mdsymlem5  29394  cdj3lem2b  29424  slmdlema  29884  pconncn  31332  cvmlift2lem1  31410  ss2mcls  31591  dfon2lem6  31817  frrlem4  31908  nofv  31935  nolesgn2o  31949  nosupbnd1lem5  31983  nn0prpw  32443  waj-ax  32538  lukshef-ax2  32539  bj-alrim  32808  bj-nexdt  32812  sucneqond  33343  ptrecube  33539  poimirlem26  33565  poimirlem29  33568  heiborlem1  33740  rngodm1dm2  33861  rngoueqz  33869  zerdivemp1x  33876  isdrngo3  33888  0rngo  33956  pridl  33966  ispridlc  33999  isdmn3  34003  dmnnzd  34004  elrelscnveq3  34381  lshpcmp  34593  omllaw  34848  dochexmidlem7  37072  lspindp5  37376  dfac21  37953  eexinst11  39050  ax6e2eq  39090  e222  39178  e111  39216  e333  39277  imarnf1pr  41624  2ffzoeq  41663  iccpartigtl  41684  iccpartgt  41688  pfxccatin12lem2  41749  pfxccatin12  41750  pfxccat3  41751  lighneallem3  41849  lighneal  41853  evenltle  41951  sgoldbeven3prm  41996  bgoldbtbndlem2  42019  nrhmzr  42198  nzerooringczr  42397  gsumpr  42464  lincdifsn  42538  snlindsntor  42585  lincresunit3lem1  42593  lincresunit3lem2  42594  lincresunit3  42595  setrec1lem2  42760
  Copyright terms: Public domain W3C validator