Theorem syl5com 63

Description: Syllogism inference with commuted antecedents.

Hypotheses

Ref	Expression
syl5com.2	|- (ph -> (ps -> ch))
syl5com.1	|- (th -> ps)

Assertion

Ref	Expression
syl5com	|- (th -> (ph -> ch))

Proof of Theorem syl5com

Step	Hyp	Ref	Expression
1		syl5com.1	. . 3 |- (th -> ps)
2	1	a1d 15	. 2 |- (th -> (ph -> ps))
3		syl5com.2	. 2 |- (ph -> (ps -> ch))
4	2, 3	sylcom 62	1 |- (th -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  pm5.18 722  ax16i 1647  mo 1787  2mo 1851  ceqsalg 2314  ceqsalgOLD 2315  cgsexg 2321  cgsex2g 2322  cgsex4g 2323  cla42egv 2366  cla43egv 2368  disjne 2919  disjneOLD 2920  ordelord 3680  trsucOLD 3753  sucssel 3763  ordsuc 3895  tfi 3937  peano5 3975  asymref2OLD 4311  funssres 4460  f1dmex 4664  fvimacnv 4778  isorel 4871  tz7.49 5168  oeworde 5268  erth 5340  dom2d 5463  enen2 5541  domen2 5543  2pwuninel 5551  ordtypelem6 5689  ordtype 5691  carden 5981  sdomsdomcard 6000  alephordi 6022  alephsucdom 6028  addcanpr 6304  xrub 7289  uzwo3lem2 7430  fseqsupcl 7704  fseqsupubi 7705  facndiv 8195  bccl2 8223  clmi1i 8346  infxpidmlem10 8830  inopn 8869  basis1 8883  tgcl 8894  tgss 8906  elcls3 8987  opnuni 9145  neibl 9154  metcnp 9165  grpass 9327  ablcom 9411  twpar2 10149  dif1enOLD 10173  indexfi 10174  fiiu2 10220  filintf 10274  fbasssin 10278  fbssint 10279  fgss 10287  usinuniop 10341  dirge 10357  exidu1 10373  uznzr 10416  shaddcl 10718  shaddclOLD 10719  shmulcl 10720  shmulclOLD 10721  hlimuniii 10741  projlem15 10833  projlem22 10840  projlem26 10844  shlej1 10988  spansnss2 11131  adj1 11494  nlelchi 11631  pjorthcoi 11741  stge0 11796  stle1 11797  stj 11807  mdsl1i 11893  irredlem1 11962  mdsymlem5 11979  ndvdssub 13710  dfon2lem6 13854  orderseqlem 13953  wfrlem4 13960  wfrlem10 13966  nofv 13998  axdenselem4 14022  waj-ax 14238  lukshef-ax2 14239  fnoprvpop 14338  fiiu 14344  domfldref 14365  f1ofi 14376  fldsqcp2 14378  surrc2 14390  set2elt 14408  inttrp 14437  cmprelid2 14447  resrelfld 14448  injrec 14461  repfuntw 14502  repcpwti 14503  prjmapcp 14507  prjnpl 14510  unprj 14511  nZdef 14527  labss1 14537  labss2 14539  domrancur1c 14550  pre2befi2 14573  supdef 14604  gaplc 14731  grpdivone 14736  rngmgmbs3 14766  rnplrnml3 14768  zerdivemp1 14785  rngridfz 14786  vecax5c 14825  svli2 14826  svs2 14829  truni3 14851  unint2t 14866  osneisi 14875  elsubops 14877  homcard 14893  subtopsin2 14907  fbaslim2 14936  iscnp3 14946  clindistop 14962  topgrpbs 14974  altretoplem2 14996  altretop 14997  cntrsetlem 14999  lvsovso3 15040  dualalg 15131  imonclem 15162  idsubfun 15206  tarax3a 15222  tartrel 15239  cptarc 15242  sexptrt 15243  tarsuc2 15245  intrtael 15256  valdom 15261  vtarsuelt 15272  inttaror 15277  fnctartar 15284  fnctartar2 15285  isseg2 15305  ordtypelem6OLD 15380  ordtypeOLD 15382  alexsub 15441  reconn 15451  fnessex 15484  neibastop1 15518  topjoin 15527  filufint 15574  fcluscomplem 15620  fclsfneii 15628  fisupg 15748  indexfiOLD 15755  sdclem2 15810  hmeoopn 15899  heiborlem11 15965  heiborlem13 15967  heiborlem15 15969  heiborlem37 15991  zerdivemp1x 16108  isdivrng3 16112  0ring 16175  pridl 16185  ispridlc 16218  isdmn3 16222  dmnnzd 16223  lubid 16807  latlem 16850  clatlem 16889  omllaw 16964  ablcomNEW 17138

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain