Theorem syl2anb 291

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 284	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 287	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylancb  418  stdcndc  846  reupick3  3448  difprsnss  3760  trin2  5061  imadiflem  5337  fnun  5364  fco  5423  f1co  5475  foco  5491  f1oun  5524  f1oco  5527  eqfunfv  5664  ftpg  5746  issmo  6346  tfrlem5  6372  ener  6838  domtr  6844  unen  6875  xpdom2  6890  mapen  6907  pm54.43  7257  axpre-lttrn  7951  axpre-mulgt0  7954  zmulcl  9379  qaddcl  9709  qmulcl  9711  rpaddcl  9752  rpmulcl  9753  rpdivcl  9754  xrltnsym  9868  xrlttri3  9872  ge0addcl  10056  ge0mulcl  10057  ge0xaddcl  10058  expclzaplem  10655  expge0  10667  expge1  10668  hashfacen  10928  qredeu  12265  nn0gcdsq  12368  mul4sq  12563  cnovex  14432  iscn2  14436  txuni  14499  txcn  14511  lgsne0  15279  mul2sq  15357