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  1773  cbvexdh  1899  repizf2  4094  issref  4929  fnun  5237  ovigg  5899  tfrlem9  6224  tfri3  6272  ordge1n0im  6341  nntri3or  6397  updjud  6975  axprecex  7712  peano5nnnn  7724  peano5nni  8747  zeo  9180  nn0ind-raph  9192  fzm1  9911  fzind2  10047  fzfig  10234  bcpasc  10544  climrecvg1n  11149  oddnn02np1  11613  oddge22np1  11614  evennn02n  11615  evennn2n  11616  gcdaddm  11708  coprmdvds1  11808  qredeq  11813  fiinopn  12210  bj-intabssel  13167  triap  13399