Theorem biimtrrdi 255

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ralnralall  4441  elinsn  4642  tppreqb  4738  sotri2  6079  sotri3  6080  somincom  6084  fnun  6599  fvmpti  6934  ovigg  7501  ndmovg  7539  onint  7733  tfindsg  7801  findsg  7837  resf1ext2b  7875  zfrep6OLD  7897  poxp2  8083  extmptsuppeq  8128  tfrlem9  8314  tfr3  8328  omlimcl  8503  oneo  8506  nnneo  8581  pssnn  9093  onomeneq  9138  inficl  9328  frmin  9664  updjud  9849  dfac2b  10044  axdc2lem  10361  axextnd  10505  canthp1lem2  10567  gchinf  10571  inatsk  10692  indpi  10821  ltaddpr2  10949  reclem2pr  10962  supsrlem  11025  axrrecex  11077  zeo  12606  nn0ind-raph  12620  fzm1  13552  fzind2  13734  addmodlteq  13899  bcpasc  14274  pr2pwpr  14432  swrdnnn0nd  14610  pwdif  15824  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  bitsfzo  16395  bezoutlem1  16499  algcvgblem  16537  coprmdvds1  16612  qredeq  16617  prmreclem2  16879  ramtcl2  16973  divsfval  17502  joinval  18332  meetval  18346  gsumval3  19873  pgpfac1lem3a  20044  fiinopn  22884  restntr  23165  lly1stc  23479  dgradd2  26251  dgrcolem2  26257  asinneg  26868  ftalem2  27055  ftalem4  27057  ftalem5  27058  bpos1lem  27263  zabsle1  27277  lgsqrmodndvds  27334  incistruhgr  29166  fusgrfis  29417  uhgrnbgr0nb  29441  cusgrrusgr  29668  wlkswwlksf1o  29965  isclwwlknx  30124  clwwlknwwlksnb  30143  clwlknf1oclwwlknlem1  30169  frgrwopreglem3  30402  frgrreg  30482  frgrregord013  30483  h1de2ctlem  31644  pjclem4a  32287  pj3lem1  32295  chrelat2i  32454  sumdmdii  32504  elim2if  32632  bnj1468  35028  bnj517  35067  acycgrislfgr  35380  axextdist  36025  funtransport  36259  mh-setindnd  36765  bj-19.21t0  37183  bj-projval  37349  areacirc  38080  rngoueqz  38307  isdmn3  38441  ax12fromc15  39397  lkrlspeqN  39663  hlrelat2  39895  ps-1  39969  dalem54  40218  cdleme42c  40964  dihmeetlem6  41801  oe0suclim  43722  sdomne0  43857  sdomne0d  43858  frege124d  44205  uneqsn  44469  iotavalb  44874  natglobalincr  47322  2reuimp  47578  afv2orxorb  47691  iccpartnel  47913  fargshiftf1  47916  nprmdvdsfacm1lem2  48099  gbowge7  48254  sbgoldbwt  48268  bgoldbtbndlem1  48296  uspgrsprf1  48638  inisegn0a  49326