Theorem syl2anb 275

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

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

Assertion

Ref	Expression
syl2anb	|- ( ( ph /\ ta ) -> th )

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 |- ( ta <-> ch )
2		syl2anb.1	. . 3 |- ( ph <-> ps )
3		syl2anb.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylanb 268	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 271	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylancb  395  reupick3  3222  difprsnss  3502  trin2  4716  imadiflem  4978  fnun  5005  fco  5056  f1co  5101  foco  5116  f1oun  5146  f1oco  5149  eqfunfv  5270  ftpg  5347  issmo  5903  tfrlem5  5930  ener  6259  domtr  6265  unen  6293  xpdom2  6305  axpre-lttrn  6958  axpre-mulgt0  6961  zmulcl  8297  qaddcl  8570  qmulcl  8572  rpaddcl  8606  rpmulcl  8607  rpdivcl  8608  xrltnsym  8714  xrlttri3  8718  ge0addcl  8850  ge0mulcl  8851  serige0  9252  expclzaplem  9279  expge0  9291  expge1  9292