Theorem syl6bir 163

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
syl6bir.1	|- ( ph -> ( ch <-> ps ) )
syl6bir.2	|- ( ch -> th )

Assertion

Ref	Expression
syl6bir	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6bir

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3 |- ( ph -> ( ch <-> ps ) )
2	1	biimprd 157	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bir.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  exdistrfor  1772  cbvexdh  1896  repizf2  4081  issref  4916  fnun  5224  ovigg  5884  tfrlem9  6209  tfri3  6257  ordge1n0im  6326  nntri3or  6382  updjud  6960  axprecex  7681  peano5nnnn  7693  peano5nni  8716  zeo  9149  nn0ind-raph  9161  fzm1  9873  fzind2  10009  fzfig  10196  bcpasc  10505  climrecvg1n  11110  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  gcdaddm  11661  coprmdvds1  11761  qredeq  11766  fiinopn  12160  bj-intabssel  12985  triap  13213