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  4515  elinsn  4710  tppreqb  4805  sotri2  6149  sotri3  6150  somincom  6154  fnun  6682  fvmpti  7015  ovigg  7578  ndmovg  7616  onint  7810  ordsucOLD  7834  tfindsg  7882  findsg  7919  resf1ext2b  7957  zfrep6  7979  poxp2  8168  extmptsuppeq  8213  tfrlem9  8425  tfr3  8439  omlimcl  8616  oneo  8619  nnneo  8693  pssnn  9208  onomeneq  9265  inficl  9465  frmin  9789  updjud  9974  dfac2b  10171  axdc2lem  10488  axextnd  10631  canthp1lem2  10693  gchinf  10697  inatsk  10818  indpi  10947  ltaddpr2  11075  reclem2pr  11088  supsrlem  11151  axrrecex  11203  zeo  12704  nn0ind-raph  12718  fzm1  13647  fzind2  13824  addmodlteq  13987  bcpasc  14360  pr2pwpr  14518  swrdnnn0nd  14694  pwdif  15904  oddnn02np1  16385  oddge22np1  16386  evennn02n  16387  evennn2n  16388  bitsfzo  16472  bezoutlem1  16576  algcvgblem  16614  coprmdvds1  16689  qredeq  16694  prmreclem2  16955  ramtcl2  17049  divsfval  17592  joinval  18422  meetval  18436  gsumval3  19925  pgpfac1lem3a  20096  fiinopn  22907  restntr  23190  lly1stc  23504  dgradd2  26308  dgrcolem2  26314  asinneg  26929  ftalem2  27117  ftalem4  27119  ftalem5  27120  bpos1lem  27326  zabsle1  27340  lgsqrmodndvds  27397  incistruhgr  29096  fusgrfis  29347  uhgrnbgr0nb  29371  cusgrrusgr  29599  wlkswwlksf1o  29899  isclwwlknx  30055  clwwlknwwlksnb  30074  clwlknf1oclwwlknlem1  30100  frgrwopreglem3  30333  frgrreg  30413  frgrregord013  30414  h1de2ctlem  31574  pjclem4a  32217  pj3lem1  32225  chrelat2i  32384  sumdmdii  32434  elim2if  32557  bnj1468  34860  bnj517  34899  acycgrislfgr  35157  axextdist  35800  funtransport  36032  bj-19.21t0  36831  bj-projval  36997  areacirc  37720  rngoueqz  37947  isdmn3  38081  ax12fromc15  38906  lkrlspeqN  39172  hlrelat2  39405  ps-1  39479  dalem54  39728  cdleme42c  40474  dihmeetlem6  41311  oe0suclim  43290  sdomne0  43426  sdomne0d  43427  frege124d  43774  uneqsn  44038  iotavalb  44449  natglobalincr  46892  2reuimp  47127  afv2orxorb  47240  iccpartnel  47425  fargshiftf1  47428  gbowge7  47750  sbgoldbwt  47764  bgoldbtbndlem1  47792  uspgrsprf1  48063