Theorem syl6bir 164

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  exdistrfor  1800  cbvexdh  1926  repizf2  4164  issref  5013  fnun  5324  ovigg  5997  tfrlem9  6322  tfri3  6370  ordge1n0im  6439  nntri3or  6496  updjud  7083  axprecex  7881  peano5nnnn  7893  peano5nni  8924  zeo  9360  nn0ind-raph  9372  fzm1  10102  fzind2  10241  fzfig  10432  bcpasc  10748  climrecvg1n  11358  oddnn02np1  11887  oddge22np1  11888  evennn02n  11889  evennn2n  11890  gcdaddm  11987  coprmdvds1  12093  qredeq  12098  fiinopn  13589  zabsle1  14485  bj-intabssel  14626  triap  14862