Theorem biimtrrdi 164

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
biimtrrdi.1	|- ( ph -> ( ch <-> ps ) )
biimtrrdi.2	|- ( ch -> th )

Assertion

Ref	Expression
biimtrrdi	|- ( ph -> ( ps -> th ) )

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 |- ( ph -> ( ch <-> ps ) )
2	1	biimprd 158	. 2 |- ( ph -> ( ps -> ch ) )
3		biimtrrdi.2	. 2 |- ( ch -> th )
4	2, 3	syl6 33	1 |- ( ph -> ( ps -> th ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  exdistrfor  1853  cbvexdh  1982  repizf2  4299  issref  5170  fnun  5489  ovigg  6209  tfrlem9  6590  tfri3  6638  ordge1n0im  6709  nntri3or  6766  updjud  7422  axprecex  8247  peano5nnnn  8259  peano5nni  9307  zeo  9751  nn0ind-raph  9763  fzm1  10507  fzind2  10658  fzfig  10867  bcpasc  11204  climrecvg1n  12114  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  bitsfzo  12722  gcdaddm  12761  coprmdvds1  12869  qredeq  12874  fiinopn  15105  zabsle1  16118  incistruhgr  16331  wlk1walkdom  16600  isclwwlknx  16657  bj-intabssel  16817  triap  17078