Theorem biimtrrdi 254

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

Hypotheses

Ref	Expression
biimtrrdi.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
biimtrrdi.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
biimtrrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem biimtrrdi

Step	Hyp	Ref	Expression
1		biimtrrdi.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 248	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  ralnralall  4466  elinsn  4662  tppreqb  4756  sotri2  6078  sotri3  6079  somincom  6083  fnun  6596  fvmpti  6929  ovigg  7494  ndmovg  7532  onint  7726  tfindsg  7794  findsg  7830  resf1ext2b  7868  zfrep6  7890  poxp2  8076  extmptsuppeq  8121  tfrlem9  8307  tfr3  8321  omlimcl  8496  oneo  8499  nnneo  8573  pssnn  9082  onomeneq  9128  inficl  9315  frmin  9645  updjud  9830  dfac2b  10025  axdc2lem  10342  axextnd  10485  canthp1lem2  10547  gchinf  10551  inatsk  10672  indpi  10801  ltaddpr2  10929  reclem2pr  10942  supsrlem  11005  axrrecex  11057  zeo  12562  nn0ind-raph  12576  fzm1  13510  fzind2  13688  addmodlteq  13853  bcpasc  14228  pr2pwpr  14386  swrdnnn0nd  14563  pwdif  15775  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  bitsfzo  16346  bezoutlem1  16450  algcvgblem  16488  coprmdvds1  16563  qredeq  16568  prmreclem2  16829  ramtcl2  16923  divsfval  17451  joinval  18281  meetval  18295  gsumval3  19786  pgpfac1lem3a  19957  fiinopn  22786  restntr  23067  lly1stc  23381  dgradd2  26172  dgrcolem2  26178  asinneg  26794  ftalem2  26982  ftalem4  26984  ftalem5  26985  bpos1lem  27191  zabsle1  27205  lgsqrmodndvds  27262  incistruhgr  29024  fusgrfis  29275  uhgrnbgr0nb  29299  cusgrrusgr  29527  wlkswwlksf1o  29824  isclwwlknx  29980  clwwlknwwlksnb  29999  clwlknf1oclwwlknlem1  30025  frgrwopreglem3  30258  frgrreg  30338  frgrregord013  30339  h1de2ctlem  31499  pjclem4a  32142  pj3lem1  32150  chrelat2i  32309  sumdmdii  32359  elim2if  32488  bnj1468  34813  bnj517  34852  acycgrislfgr  35125  axextdist  35773  funtransport  36005  bj-19.21t0  36804  bj-projval  36970  areacirc  37693  rngoueqz  37920  isdmn3  38054  ax12fromc15  38884  lkrlspeqN  39150  hlrelat2  39382  ps-1  39456  dalem54  39705  cdleme42c  40451  dihmeetlem6  41288  oe0suclim  43250  sdomne0  43386  sdomne0d  43387  frege124d  43734  uneqsn  43998  iotavalb  44403  natglobalincr  46858  2reuimp  47099  afv2orxorb  47212  iccpartnel  47422  fargshiftf1  47425  gbowge7  47747  sbgoldbwt  47761  bgoldbtbndlem1  47789  uspgrsprf1  48131  inisegn0a  48820