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  4478  elinsn  4674  tppreqb  4769  sotri2  6102  sotri3  6103  somincom  6107  fnun  6632  fvmpti  6967  ovigg  7534  ndmovg  7572  onint  7766  ordsucOLD  7789  tfindsg  7837  findsg  7873  resf1ext2b  7911  zfrep6  7933  poxp2  8122  extmptsuppeq  8167  tfrlem9  8353  tfr3  8367  omlimcl  8542  oneo  8545  nnneo  8619  pssnn  9132  onomeneq  9178  inficl  9376  frmin  9702  updjud  9887  dfac2b  10084  axdc2lem  10401  axextnd  10544  canthp1lem2  10606  gchinf  10610  inatsk  10731  indpi  10860  ltaddpr2  10988  reclem2pr  11001  supsrlem  11064  axrrecex  11116  zeo  12620  nn0ind-raph  12634  fzm1  13568  fzind2  13746  addmodlteq  13911  bcpasc  14286  pr2pwpr  14444  swrdnnn0nd  14621  pwdif  15834  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  bitsfzo  16405  bezoutlem1  16509  algcvgblem  16547  coprmdvds1  16622  qredeq  16627  prmreclem2  16888  ramtcl2  16982  divsfval  17510  joinval  18336  meetval  18350  gsumval3  19837  pgpfac1lem3a  20008  fiinopn  22788  restntr  23069  lly1stc  23383  dgradd2  26174  dgrcolem2  26180  asinneg  26796  ftalem2  26984  ftalem4  26986  ftalem5  26987  bpos1lem  27193  zabsle1  27207  lgsqrmodndvds  27264  incistruhgr  29006  fusgrfis  29257  uhgrnbgr0nb  29281  cusgrrusgr  29509  wlkswwlksf1o  29809  isclwwlknx  29965  clwwlknwwlksnb  29984  clwlknf1oclwwlknlem1  30010  frgrwopreglem3  30243  frgrreg  30323  frgrregord013  30324  h1de2ctlem  31484  pjclem4a  32127  pj3lem1  32135  chrelat2i  32294  sumdmdii  32344  elim2if  32473  bnj1468  34836  bnj517  34875  acycgrislfgr  35139  axextdist  35787  funtransport  36019  bj-19.21t0  36818  bj-projval  36984  areacirc  37707  rngoueqz  37934  isdmn3  38068  ax12fromc15  38898  lkrlspeqN  39164  hlrelat2  39397  ps-1  39471  dalem54  39720  cdleme42c  40466  dihmeetlem6  41303  oe0suclim  43266  sdomne0  43402  sdomne0d  43403  frege124d  43750  uneqsn  44014  iotavalb  44419  natglobalincr  46875  2reuimp  47116  afv2orxorb  47229  iccpartnel  47439  fargshiftf1  47442  gbowge7  47764  sbgoldbwt  47778  bgoldbtbndlem1  47806  uspgrsprf1  48135  inisegn0a  48824