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  1793  cbvexdh  1919  repizf2  4148  issref  4993  fnun  5304  ovigg  5973  tfrlem9  6298  tfri3  6346  ordge1n0im  6415  nntri3or  6472  updjud  7059  axprecex  7842  peano5nnnn  7854  peano5nni  8881  zeo  9317  nn0ind-raph  9329  fzm1  10056  fzind2  10195  fzfig  10386  bcpasc  10700  climrecvg1n  11311  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  gcdaddm  11939  coprmdvds1  12045  qredeq  12050  fiinopn  12796  zabsle1  13694  bj-intabssel  13824  triap  14061