Theorem sylancom 477

Description: Syllogism inference with commutation of antecents.

Hypotheses

Ref	Expression
sylancom.1	⊢ ((φ ⋀ ψ) → χ)
sylancom.2	⊢ ((χ ⋀ ψ) → θ)

Assertion

Ref	Expression
sylancom	⊢ ((φ ⋀ ψ) → θ)

Proof of Theorem sylancom

Step	Hyp	Ref	Expression
1		sylancom.2	. 2 ⊢ ((χ ⋀ ψ) → θ)
2		sylancom.1	. 2 ⊢ ((φ ⋀ ψ) → χ)
3		pm3.27 323	. 2 ⊢ ((φ ⋀ ψ) → ψ)
4	1, 2, 3	sylanc 473	1 ⊢ ((φ ⋀ ψ) → θ)

Syntax hints:   → wi 3   ⋀ wa 223

This theorem is referenced by:  ordin 2984  releldm 3353  fnbr 3597  fimacnvdisj 3656  rdglimt 3955  eqop 4111  f1oeng 4402  onomeneq 4526  unfilem3 4564  ltdiv23t 5901  lediv23t 5902  recgt1it 5909  avglet 6053  uzindOLD 6217  shftcan2t 6361  fzneuzt 6526  climmullem3 7129  demoivre 7492  xpnnen 7507  infxpidmlem12 7571  cctop 7656  cmsss 8001  grpidinv 8056  ghgrpilem3 8138  imsmetlem 8326  ipasslem1 8493  ip2eqi 8520  pstr 8655  hvpncant 8910  pjidt 9642  hmopret 9849  eigvalclt 9887  leopnmidt 10073  superpos 10284  cvp 10305  cnvtr 10617

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