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  1788  cbvexdh  1914  repizf2  4141  issref  4986  fnun  5294  ovigg  5962  tfrlem9  6287  tfri3  6335  ordge1n0im  6404  nntri3or  6461  updjud  7047  axprecex  7821  peano5nnnn  7833  peano5nni  8860  zeo  9296  nn0ind-raph  9308  fzm1  10035  fzind2  10174  fzfig  10365  bcpasc  10679  climrecvg1n  11289  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  gcdaddm  11917  coprmdvds1  12023  qredeq  12028  fiinopn  12642  zabsle1  13540  bj-intabssel  13670  triap  13908