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  4474  elinsn  4670  tppreqb  4765  sotri2  6090  sotri3  6091  somincom  6095  fnun  6614  fvmpti  6949  ovigg  7514  ndmovg  7552  onint  7746  ordsucOLD  7769  tfindsg  7817  findsg  7853  resf1ext2b  7891  zfrep6  7913  poxp2  8099  extmptsuppeq  8144  tfrlem9  8330  tfr3  8344  omlimcl  8519  oneo  8522  nnneo  8596  pssnn  9109  onomeneq  9155  inficl  9352  frmin  9678  updjud  9863  dfac2b  10060  axdc2lem  10377  axextnd  10520  canthp1lem2  10582  gchinf  10586  inatsk  10707  indpi  10836  ltaddpr2  10964  reclem2pr  10977  supsrlem  11040  axrrecex  11092  zeo  12596  nn0ind-raph  12610  fzm1  13544  fzind2  13722  addmodlteq  13887  bcpasc  14262  pr2pwpr  14420  swrdnnn0nd  14597  pwdif  15810  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  bitsfzo  16381  bezoutlem1  16485  algcvgblem  16523  coprmdvds1  16598  qredeq  16603  prmreclem2  16864  ramtcl2  16958  divsfval  17486  joinval  18312  meetval  18326  gsumval3  19813  pgpfac1lem3a  19984  fiinopn  22764  restntr  23045  lly1stc  23359  dgradd2  26150  dgrcolem2  26156  asinneg  26772  ftalem2  26960  ftalem4  26962  ftalem5  26963  bpos1lem  27169  zabsle1  27183  lgsqrmodndvds  27240  incistruhgr  28982  fusgrfis  29233  uhgrnbgr0nb  29257  cusgrrusgr  29485  wlkswwlksf1o  29782  isclwwlknx  29938  clwwlknwwlksnb  29957  clwlknf1oclwwlknlem1  29983  frgrwopreglem3  30216  frgrreg  30296  frgrregord013  30297  h1de2ctlem  31457  pjclem4a  32100  pj3lem1  32108  chrelat2i  32267  sumdmdii  32317  elim2if  32446  bnj1468  34809  bnj517  34848  acycgrislfgr  35112  axextdist  35760  funtransport  35992  bj-19.21t0  36791  bj-projval  36957  areacirc  37680  rngoueqz  37907  isdmn3  38041  ax12fromc15  38871  lkrlspeqN  39137  hlrelat2  39370  ps-1  39444  dalem54  39693  cdleme42c  40439  dihmeetlem6  41276  oe0suclim  43239  sdomne0  43375  sdomne0d  43376  frege124d  43723  uneqsn  43987  iotavalb  44392  natglobalincr  46848  2reuimp  47089  afv2orxorb  47202  iccpartnel  47412  fargshiftf1  47415  gbowge7  47737  sbgoldbwt  47751  bgoldbtbndlem1  47779  uspgrsprf1  48108  inisegn0a  48797