Theorem sylancom 477

Description: Syllogism inference with commutation of antecents.

Hypotheses

Ref	Expression
sylancom.1	|- ((ph /\ ps) -> ch)
sylancom.2	|- ((ch /\ ps) -> th)

Assertion

Ref	Expression
sylancom	|- ((ph /\ ps) -> th)

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.2	. 2 |- ((ch /\ ps) -> th)
2		sylancom.1	. 2 |- ((ph /\ ps) -> ch)
3		pm3.27 323	. 2 |- ((ph /\ ps) -> ps)
4	1, 2, 3	sylanc 473	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ordin 2983  releldm 3352  fnbr 3596  fimacnvdisj 3655  rdglimt 3954  eqop 4110  f1oeng 4401  onomeneq 4525  unfilem3 4562  ltdiv23t 5894  lediv23t 5895  recgt1it 5902  avglet 6046  uzindOLD 6210  shftcan2t 6354  fzneuzt 6519  climmullem3 7122  demoivre 7485  xpnnen 7500  infxpidmlem12 7564  cctop 7649  cmsss 7994  grpidinv 8049  ghgrpilem3 8131  imsmetlem 8319  ipasslem1 8486  ip2eqi 8513  pstr 8648  hvpncant 8903  pjidt 9635  hmopret 9842  eigvalclt 9880  leopnmidt 10066  superpos 10276  cvp 10297  cnvtr 10609

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain