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  9309  zeo  9755  nn0ind-raph  9767  fzm1  10517  fzind2  10668  fzfig  10880  bcpasc  11218  climrecvg1n  12130  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  bitsfzo  12738  gcdaddm  12777  coprmdvds1  12885  qredeq  12890  fiinopn  15154  bpos1lem  16207  zabsle1  16216  incistruhgr  16429  wlk1walkdom  16698  isclwwlknx  16755  bj-intabssel  16915  triap  17176