Theorem sylancom 475

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 471	1 |- ((ph /\ ps) -> th)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ordin 2977  releldm 3346  fnbr 3590  fimacnvdisj 3649  rdglimt 3948  eqop 4104  f1oeng 4395  onomeneq 4519  unfilem3 4550  ltdiv23t 5892  lediv23t 5893  recgt1it 5900  avglet 6044  uzindOLD 6208  shftcan2t 6353  fzneuzt 6518  climmullem3 7122  demoivre 7484  xpnnen 7499  infxpidmlem12 7563  cctop 7652  cmsss 7997  grpidinv 8052  ghgrpilem3 8135  imsmetlem 8323  ipasslem1 8490  ip2eqi 8517  pstr 8652  hvpncant 8908  pjidt 9640  hmopret 9847  eigvalclt 9885  leopnmidt 10071  superpos 10281  cvp 10302  cnvtr 10638

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