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 1269  mo 1392  2mo 1446  ceqsalg 1822  cgsexg 1828  cgsex2g 1829  cgsex4g 1830  cla42egv 1861  cla43egv 1863  disjne 2312  ordelord 2966  trsuc 3051  ordsuc 3061  sucssel 3066  tfi 3122  peano5 3149  asymref2 3436  funssres 3548  f1dmex 3705  fvimacnv 3800  isorel 3889  tz7.49 3954  oeworde 4213  erth 4275  dom2d 4394  enen2 4467  domen2 4469  2pwuninel 4476  carden 4814  sdomsdomcard 4831  alephordi 4857  alephsucdom 4863  addcanpr 5135  xrub 6037  uzwo3lem2 6175  fseqsupcl 6470  fseqsupub 6471  facndivt 6895  bccl2t 6924  clmi1 7039  infxpidmlem10 7521  inopnt 7560  basis1t 7574  tgclt 7584  tgsst 7596  elcls3 7671  opnuni 7830  neibl 7839  metcnp 7849  grpass 8009  ablcom 8066  shaddclt 9040  shaddcltOLD 9041  shmulclt 9042  shmulcltOLD 9043  hlimunii 9063  projlem15 9155  projlem22 9162  projlem26 9166  shlej1t 9310  spansnss2t 9455  adjt 9814  nlelch 9950  pjorthco 10053  stge0t 10107  stle1t 10108  stjt 10118  mdsl1 10204  irredlem1 10273  mdsymlem5 10290  fiiu 10408  fiiu2 10436  homcard 10485  filintf 10502  imonclem 10655

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

Copyright terms: Public domain