Theorem sylan2b 347

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2b	|- ((ph /\ th) -> ch)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ((ph /\ ps) -> ch)
2		sylan2b.2	. . 3 |- (th <-> ps)
3	2	biimp 133	. 2 |- (th -> ps)
4	1, 3	sylan2 346	1 |- ((ph /\ th) -> ch)

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

This theorem is referenced by:  syl2anb 350  bm1.1 1088  psssstr 1576  reuss 1577  reupick 1578  reuuni1 1955  opabss 2100  poirr 2133  wefrc 2195  fvopab2 2878  fnressn 2897  isowe 2941  iinon 2948  tfrlem2 2950  oawordeulem 3156  nnmordi 3188  omsmolem 3195  erref 3212  mapdom2 3389  mapunen 3397  ssnn 3429  inf3lem5 3468  r1pwcl 3530  aceq5lem4 3561  addclpi 3814  addnidpi 3822  recexsr 4010  divdivdivt 4265  addgt0 4323  uzind2 4604  uzwo2 4606  ruclem26 4910  hsn0elch 5155  shscl 5282  chcv1t 5751

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