Theorem biimtrrdi 256

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 250	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ralnralall  4467  elinsn  4669  tppreqb  4765  sotri2  6116  sotri3  6117  somincom  6121  fnun  6635  fvmpti  6974  ovigg  7541  ndmovg  7579  onint  7773  tfindsg  7841  findsg  7878  resf1ext2b  7916  zfrep6OLD  7936  poxp2  8123  extmptsuppeq  8168  tfrlem9  8356  tfr3  8370  omlimcl  8547  oneo  8550  nnneo  8625  pssnn  9137  onomeneq  9182  inficl  9371  frmin  9707  updjud  9892  dfac2b  10087  axdc2lem  10405  axextnd  10549  canthp1lem2  10611  gchinf  10615  inatsk  10736  indpi  10865  ltaddpr2  10993  reclem2pr  11006  supsrlem  11069  axrrecex  11121  zeo  12659  nn0ind-raph  12673  fzm1  13612  fzind2  13794  addmodlteq  13959  bcpasc  14334  pr2pwpr  14492  swrdnnn0nd  14670  pwdif  15898  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  bitsfzo  16469  bezoutlem1  16573  algcvgblem  16611  coprmdvds1  16686  qredeq  16691  prmreclem2  16953  ramtcl2  17047  divsfval  17577  joinval  18407  meetval  18421  gsumval3  19947  pgpfac1lem3a  20118  fiinopn  22958  restntr  23239  lly1stc  23553  dgradd2  26325  dgrcolem2  26331  asinneg  26948  ftalem2  27135  ftalem4  27137  ftalem5  27138  bpos1lem  27343  zabsle1  27357  lgsqrmodndvds  27414  incistruhgr  29277  fusgrfis  29528  uhgrnbgr0nb  29552  cusgrrusgr  29779  wlkswwlksf1o  30076  isclwwlknx  30235  clwwlknwwlksnb  30254  clwlknf1oclwwlknlem1  30280  frgrwopreglem3  30513  frgrreg  30593  frgrregord013  30594  h1de2ctlem  31755  pjclem4a  32398  pj3lem1  32406  chrelat2i  32565  sumdmdii  32615  elim2if  32740  bnj1468  35138  bnj517  35177  acycgrislfgr  35499  axextdist  36144  funtransport  36378  mh-setindnd  36894  bj-19.21t0  37312  bj-projval  37478  areacirc  38209  rngoueqz  38436  isdmn3  38570  ax12fromc15  39526  lkrlspeqN  39792  hlrelat2  40024  ps-1  40098  dalem54  40347  cdleme42c  41093  dihmeetlem6  41930  oe0suclim  43851  sdomne0  43986  sdomne0d  43987  frege124d  44334  uneqsn  44598  iotavalb  45003  natglobalincr  47450  2reuimp  47706  afv2orxorb  47819  iccpartnel  48041  fargshiftf1  48044  nprmdvdsfacm1lem2  48227  gbowge7  48382  sbgoldbwt  48396  bgoldbtbndlem1  48424  uspgrsprf1  48766  inisegn0a  49454