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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylancb  422  stdcndc  857  reupick3  3518  difprsnss  3853  trin2  5182  fundif  5428  imadiflem  5463  fnun  5492  fco  5555  f1co  5613  foco  5629  f1oun  5662  f1oco  5665  eqfunfv  5814  ftpg  5902  issmo  6563  tfrlem5  6589  ener  7070  domtr  7076  unen  7109  xpdom2  7133  mapen  7150  pm54.43  7542  axpre-lttrn  8257  axpre-mulgt0  8260  zmulcl  9709  qaddcl  10051  qmulcl  10053  rpaddcl  10095  rpmulcl  10096  rpdivcl  10097  xrltnsym  10212  xrlttri3  10216  ge0addcl  10400  ge0mulcl  10401  ge0xaddcl  10402  expclzaplem  11021  expge0  11033  expge1  11034  hashfacen  11306  qredeu  12900  nn0gcdsq  13005  mul4sq  13202  ballotfilem2  13286  cnovex  15422  iscn2  15426  txuni  15489  txcn  15501  efnnfsumcl  16239  efchtqdvds  16265  lgsne0  16362  mul2sq  16440