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  4454  elinsn  4655  tppreqb  4749  sotri2  6084  sotri3  6085  somincom  6089  fnun  6604  fvmpti  6938  ovigg  7503  ndmovg  7541  onint  7735  tfindsg  7803  findsg  7839  resf1ext2b  7877  zfrep6OLD  7899  poxp2  8084  extmptsuppeq  8129  tfrlem9  8315  tfr3  8329  omlimcl  8504  oneo  8507  nnneo  8582  pssnn  9094  onomeneq  9139  inficl  9329  frmin  9662  updjud  9847  dfac2b  10042  axdc2lem  10359  axextnd  10503  canthp1lem2  10565  gchinf  10569  inatsk  10690  indpi  10819  ltaddpr2  10947  reclem2pr  10960  supsrlem  11023  axrrecex  11075  zeo  12579  nn0ind-raph  12593  fzm1  13524  fzind2  13705  addmodlteq  13870  bcpasc  14245  pr2pwpr  14403  swrdnnn0nd  14581  pwdif  15792  oddnn02np1  16276  oddge22np1  16277  evennn02n  16278  evennn2n  16279  bitsfzo  16363  bezoutlem1  16467  algcvgblem  16505  coprmdvds1  16580  qredeq  16585  prmreclem2  16846  ramtcl2  16940  divsfval  17469  joinval  18299  meetval  18313  gsumval3  19840  pgpfac1lem3a  20011  fiinopn  22844  restntr  23125  lly1stc  23439  dgradd2  26214  dgrcolem2  26220  asinneg  26836  ftalem2  27024  ftalem4  27026  ftalem5  27027  bpos1lem  27233  zabsle1  27247  lgsqrmodndvds  27304  incistruhgr  29136  fusgrfis  29387  uhgrnbgr0nb  29411  cusgrrusgr  29639  wlkswwlksf1o  29936  isclwwlknx  30095  clwwlknwwlksnb  30114  clwlknf1oclwwlknlem1  30140  frgrwopreglem3  30373  frgrreg  30453  frgrregord013  30454  h1de2ctlem  31615  pjclem4a  32258  pj3lem1  32266  chrelat2i  32425  sumdmdii  32475  elim2if  32603  bnj1468  34994  bnj517  35033  acycgrislfgr  35340  axextdist  35985  funtransport  36219  mh-setindnd  36725  bj-19.21t0  37135  bj-projval  37301  areacirc  38025  rngoueqz  38252  isdmn3  38386  ax12fromc15  39342  lkrlspeqN  39608  hlrelat2  39840  ps-1  39914  dalem54  40163  cdleme42c  40909  dihmeetlem6  41746  oe0suclim  43708  sdomne0  43843  sdomne0d  43844  frege124d  44191  uneqsn  44455  iotavalb  44860  natglobalincr  47309  2reuimp  47549  afv2orxorb  47662  iccpartnel  47872  fargshiftf1  47875  gbowge7  48197  sbgoldbwt  48211  bgoldbtbndlem1  48239  uspgrsprf1  48581  inisegn0a  49269