Theorem syl6bir 162

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 156	. 2 |- ( ph -> ( ps -> ch ) )
3		syl6bir.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  exdistrfor  1728  cbvexdh  1849  repizf2  3997  issref  4814  fnun  5120  ovigg  5765  tfrlem9  6084  tfri3  6132  ordge1n0im  6200  nntri3or  6254  updjud  6773  axprecex  7415  peano5nnnn  7427  peano5nni  8425  zeo  8851  nn0ind-raph  8863  fzm1  9514  fzind2  9650  fzfig  9837  bcpasc  10174  climrecvg1n  10737  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  gcdaddm  11253  coprmdvds1  11351  qredeq  11356  fiinopn  11601  bj-intabssel  11689