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  1780  cbvexdh  1906  repizf2  4123  issref  4968  fnun  5276  ovigg  5941  tfrlem9  6266  tfri3  6314  ordge1n0im  6383  nntri3or  6440  updjud  7026  axprecex  7800  peano5nnnn  7812  peano5nni  8836  zeo  9269  nn0ind-raph  9281  fzm1  10002  fzind2  10138  fzfig  10329  bcpasc  10640  climrecvg1n  11245  oddnn02np1  11771  oddge22np1  11772  evennn02n  11773  evennn2n  11774  gcdaddm  11868  coprmdvds1  11968  qredeq  11973  fiinopn  12413  bj-intabssel  13374  triap  13611