Theorem sylanb 449

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylanb	|- ((th /\ ps) -> ch)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylanb.2	. . 3 |- (th <-> ph)
3	2	biimp 151	. 2 |- (th -> ph)
4	1, 3	sylan 448	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  syl2anb 455  2euex 1434  2exeu 1439  eqtr2t 1485  sspsstr 2141  disjne 2305  ordon 2977  ordsucss 3059  ordsucelsuc 3063  funex 3594  fssres 3628  fvimacnvi 3789  tz7.48lem 3940  1st2nd 4092  oeworde 4204  nnmsucr 4224  erref 4259  mapxpen 4475  php 4493  php3 4495  php4 4496  omsucdom 4502  isfinite2 4523  fodomfi 4540  brdom3 4773  cfeq0 4886  pre-axsup 5263  divmul13t 5738  lemuldivt 5824  uzindOLD 6156  qbtwnxr 6217  faclbnd 6882  faclbnd3 6884  fsum0clt 6954  ser0clt 6984  ser1clt 6985  binomlem5 7008  climaddlem3 7052  climmullem8 7063  climcmplem 7073  isumnn0nna 7143  mulc1cncf 7214  ruclem13 7465  opnin 7809  fsumcnlem 7923  grpidinvlem3 7984  mulid 8069  ipasslem3 8423  hilid 8949  occllem6 9094  spanun 9382  5oalem3 9518  5oalem5 9520  mdslmd1lem2 10161

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