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  1968  sbequ2OLD  2243  axc16i  2436  eupickbi  2638  ceqsalgALT  3477  cgsexg  3487  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spcegv  3555  spc2egv  3557  disjne  4413  uneqdifeq  4449  preqsnd  4815  preq12nebg  4819  opthprneg  4821  dfiun2g  4989  pocl  5550  relresfld  6225  unixpid  6233  ordnbtwn  6407  sucssel  6409  ordelinel  6415  funmo  6512  fvimacnv  6999  2f1fvneq  7202  ordsuc  7739  ordsucOLD  7740  tfi  7780  focdmex  7879  f1ovv  7881  opreuopreu  7957  frrlem4  8188  wfrlem4OLD  8226  wfrlem10OLD  8232  tz7.49  8359  oeworde  8508  fsetprcnex  8734  dom2d  8867  findcard  9041  fisupg  9169  dffi3  9301  noinfep  9530  cantnflem2  9560  ttrcltr  9586  tcmin  9611  rankr1ag  9672  rankunb  9720  rankxpsuc  9752  alephordi  9944  alephsucdom  9949  alephinit  9965  dfac9  10006  ackbij2lem4  10112  cff1  10128  cfslbn  10137  cfcoflem  10142  cfcof  10144  infpssrlem5  10177  isfin7-2  10266  acncc  10310  domtriomlem  10312  axdc3lem2  10321  ttukeylem1  10379  iundom2g  10410  axpowndlem3  10469  wunex2  10608  grupr  10667  gruiun  10669  eltskm  10713  nqereu  10799  addcanpr  10916  axpre-sup  11039  relin01  11613  nneo  12518  zeo2  12521  xrub  13160  uznfz  13453  difelfzle  13483  ssfzo12  13594  facndiv  14116  hashgt12el2  14251  hash2prde  14297  hash2pwpr  14303  hashle2prv  14305  fi1uzind  14324  swrdswrd  14525  pfxccatin12lem2  14551  pfxccatin12  14553  pfxccat3  14554  cshwidxmod  14623  2cshwcshw  14646  fsumcom2  15594  fprodss  15766  fprodcom2  15802  sumodd  16205  ndvdssub  16226  eucalglt  16396  prmind2  16496  coprm  16522  prmdiveq  16593  prmdvdsprmop  16850  prmgaplem5  16862  cicsym  17622  drsdir  18126  lublecllem  18184  istos  18242  tsrlin  18409  dirge  18427  mhmlin  18544  issubg2  18876  nsgbi  18892  symgextf1lem  19135  sylow2a  19331  gsumpr  19662  issubrg2  20166  abvmul  20212  abvtri  20213  lmodlema  20251  rmodislmodlem  20313  rmodislmod  20314  rmodislmodOLD  20315  lspsnel6  20379  lmhmlin  20420  lbsind  20465  0ringnnzr  20663  0ring01eq  20665  01eq0ring  20666  ipcj  20962  obsip  21051  lindsss  21154  mamufacex  21661  mavmulsolcl  21823  slesolvec  21951  inopn  22171  basis1  22223  tgss  22241  tgcl  22242  elcls3  22357  neindisj2  22397  cncls  22548  1stcelcls  22735  qtoptop2  22973  nrmr0reg  23023  fbasssin  23110  fbfinnfr  23115  fbunfip  23143  filufint  23194  uffix  23195  ufinffr  23203  ufilen  23204  fmfnfmlem1  23228  flftg  23270  alexsubALT  23325  xmeteq0  23614  blssexps  23702  blssex  23703  mopni3  23773  neibl  23780  metss  23787  metcnp3  23819  nmvs  23963  iccntr  24107  reconnlem2  24113  lebnumlem3  24249  caubl  24595  bcthlem5  24615  ovolunlem1  24784  voliunlem1  24837  volsuplem  24842  ellimc3  25166  logbgcd1irr  26067  lgsqrmodndvds  26624  gausslemma2dlem0i  26635  2lgsoddprmlem3  26685  dchrisumlema  26759  nofv  26928  nolesgn2o  26942  nogesgn1o  26944  nosupbnd1lem5  26983  umgrnloopv  27856  usgrnloopvALT  27948  umgrres1lem  28057  upgrres1  28060  nbuhgr  28090  cplgrop  28184  fusgrregdegfi  28316  g0wlk0  28399  wlkdlem2  28430  upgrwlkdvdelem  28483  crctcshwlkn0lem3  28556  crctcshwlkn0lem5  28558  wspn0  28668  umgrwwlks2on  28701  elwspths2spth  28711  clwlkclwwlklem2a  28741  clwlkclwwlklem3  28744  clwwlkn1loopb  28786  clwwlknonwwlknonb  28849  clwwlknonex2lem2  28851  3cyclfrgrrn2  29030  frgrncvvdeqlem8  29049  frgrwopregasn  29059  frgrwopregbsn  29060  frgrwopreg1  29061  frgrwopreg2  29062  frgrregord013  29138  frgrogt3nreg  29140  ablocom  29289  ubthlem1  29611  shaddcl  29958  shmulcl  29959  spansnss2  30316  cnopc  30654  cnfnc  30671  adj1  30674  pjorthcoi  30910  stj  30976  mdsl1i  31062  chirredlem1  31131  mdsymlem5  31148  cdj3lem2b  31178  slmdlema  31833  isprmidlc  32010  pconncn  33592  cvmlift2lem1  33670  fmla0xp  33751  ss2mcls  33936  dfon2lem6  34154  addsprop  34279  waj-ax  34782  lukshef-ax2  34783  bj-alrim  35054  bj-nexdt  35058  sucneqond  35732  rdgssun  35745  ptrecube  35974  poimirlem26  36000  poimirlem29  36003  heiborlem1  36166  rngodm1dm2  36287  rngoueqz  36295  zerdivemp1x  36302  isdrngo3  36314  0rngo  36382  pridl  36392  ispridlc  36425  isdmn3  36429  dmnnzd  36430  elrelscnveq3  36849  lshpcmp  37346  omllaw  37601  dochexmidlem7  39825  lspindp5  40129  fsuppind  40634  dfac21  41259  eexinst11  42574  ax6e2eq  42604  e222  42683  e111  42721  e333  42780  natlocalincr  44870  tworepnotupword  44880  imarnf1pr  45269  2ffzoeq  45315  iccpartigtl  45370  iccpartgt  45374  lighneallem3  45554  lighneal  45558  requad1  45569  evenltle  45664  fppr2odd  45678  sgoldbeven3prm  45730  bgoldbtbndlem2  45753  isomuspgrlem2b  45776  nrhmzr  45926  nzerooringczr  46125  lincdifsn  46260  lindslinindimp2lem4  46297  snlindsntor  46307  lincresunit3lem1  46315  lincresunit3lem2  46316  f002  46675  setrec1lem2  46888
  Copyright terms: Public domain W3C validator