Theorem syl5com 52

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 12	. 2 |- (th -> (ph -> ps))
3		syl5com.2	. 2 |- (ph -> (ps -> ch))
4	2, 3	sylcom 51	1 |- (th -> (ph -> ch))

Syntax hints:   -> wi 3

This theorem is referenced by:  ax16i 1308  mo 1432  2mo 1487  ceqsalg 1871  cgsexg 1877  cgsex2g 1878  cgsex4g 1879  cla42egv 1910  cla43egv 1912  disjne 2368  ordelord 2997  trsuc 3056  sucssel 3064  ordsuc 3171  tfi 3207  peano5 3241  asymref2 3532  funssres 3657  f1dmex 3821  fvimacnv 3919  isorel 4008  tz7.49 4260  oeworde 4356  erth 4422  dom2d 4545  enen2 4623  domen2 4625  2pwuninel 4632  carden 4979  sdomsdomcard 4998  alephordi 5024  alephsucdom 5030  addcanpr 5306  xrub 6248  uzwo3lem2 6389  fseqsupcl 6656  fseqsupubi 6657  facndiv 7146  bccl2 7174  clmi1i 7289  infxpidmlem10 7773  inopn 7812  basis1 7826  tgcl 7836  tgss 7848  elcls3 7921  opnuni 8078  neibl 8087  metcnp 8098  grpass 8260  ablcom 8344  shaddcl 9361  shaddclOLD 9362  shmulcl 9363  shmulclOLD 9364  hlimuniii 9384  projlem15 9476  projlem22 9483  projlem26 9487  shlej1 9631  spansnss2 9774  adj1 10137  nlelchi 10273  pjorthcoi 10377  stge0 10432  stle1 10433  stj 10443  mdsl1i 10529  irredlem1 10599  mdsymlem5 10616  fiiu 10738  domfldref 10765  twpar2 10773  f1ofi 10778  fldsqcp2 10780  set2elt 10827  labss1 10837  labss2 10839  fiiu2 10852  exidu1 10902  rngmgmbs3 10944  rnplrnml3 10950  uznzr 10967  truni3 11001  osneisi 11018  homcard 11045  subtopsin2 11067  filintf 11081  usinuniop 11128  clindistop 11131  altretoplem2 11143  altretop 11144  imonclem 11268  idsubfun 11312  ordtypelem6 11432  ordtype 11434  alexsub 11500  reconn 11512  fnessex 11545  neibastop1 11579  topjoin 11588  fbasssin 11625  fbssint 11626  fgss 11634  filufint 11659  fcluscomplem 11732  fclsfneii 11740  dirge 11754  dif1en 11833  fisupg 11839  indexf 11847  sdclem2 11876  hmeoopn 11960  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem37 12047

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

Copyright terms: Public domain