Theorem sylan2b 461

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- (ph <-> ch)
2	1	biimpi 186	. 2 |- (ph -> ch)
3		sylan2b.2	. 2 |- ((ps /\ ch) -> th)
4	2, 3	sylan2 460	1 |- ((ps /\ ph) -> th)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

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

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  syl2anb  465  bm1.1  2338  eqtr3  2372  morex  3021  psssstr  3376  reuss2  3536  reupick  3540  reximdva0  3562  rabsneu  3796  reiota2  4369  nnsucelr  4429  nndisjeq  4430  prepeano4  4452  lefinlteq  4464  ltlefin  4469  ncfinraise  4482  sfindbl  4531  nulnnn  4557  xpcan  5058  fnfco  5238  fun11iun  5306  tz6.12-1  5345  fnressn  5439  fndmeng  6047