Theorem sylanb 344

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 133	. 2 |- (th -> ph)
4	1, 3	sylan 343	1 |- ((th /\ ps) -> ch)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  syl2anb 350  2euex 1061  2exeu 1066  sspsstr 1575  moop2 1910  ordon 2238  ordsucss 2320  ordsucelsuc 2324  fssres 2764  tz7.48lem 2993  nnmsucr 3182  erref 3212  mapxpen 3390  php 3409  php3 3411  php4 3412  omsucdom 3418  isfinite2 3437  aceq5lem4 3561  axsup 4088  divdivdivt 4265  uzind 4603  nnwo 4607  ruclem13 4897  occllem6 5185  spanun 5450  5oalem3 5546  5oalem5 5548

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org