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  4462  elinsn  4660  tppreqb  4754  sotri2  6075  sotri3  6076  somincom  6080  fnun  6595  fvmpti  6928  ovigg  7491  ndmovg  7529  onint  7723  tfindsg  7791  findsg  7827  resf1ext2b  7865  zfrep6  7887  poxp2  8073  extmptsuppeq  8118  tfrlem9  8304  tfr3  8318  omlimcl  8493  oneo  8496  nnneo  8570  pssnn  9078  onomeneq  9123  inficl  9309  frmin  9642  updjud  9827  dfac2b  10022  axdc2lem  10339  axextnd  10482  canthp1lem2  10544  gchinf  10548  inatsk  10669  indpi  10798  ltaddpr2  10926  reclem2pr  10939  supsrlem  11002  axrrecex  11054  zeo  12559  nn0ind-raph  12573  fzm1  13507  fzind2  13688  addmodlteq  13853  bcpasc  14228  pr2pwpr  14386  swrdnnn0nd  14564  pwdif  15775  oddnn02np1  16259  oddge22np1  16260  evennn02n  16261  evennn2n  16262  bitsfzo  16346  bezoutlem1  16450  algcvgblem  16488  coprmdvds1  16563  qredeq  16568  prmreclem2  16829  ramtcl2  16923  divsfval  17451  joinval  18281  meetval  18295  gsumval3  19819  pgpfac1lem3a  19990  fiinopn  22816  restntr  23097  lly1stc  23411  dgradd2  26201  dgrcolem2  26207  asinneg  26823  ftalem2  27011  ftalem4  27013  ftalem5  27014  bpos1lem  27220  zabsle1  27234  lgsqrmodndvds  27291  incistruhgr  29057  fusgrfis  29308  uhgrnbgr0nb  29332  cusgrrusgr  29560  wlkswwlksf1o  29857  isclwwlknx  30016  clwwlknwwlksnb  30035  clwlknf1oclwwlknlem1  30061  frgrwopreglem3  30294  frgrreg  30374  frgrregord013  30375  h1de2ctlem  31535  pjclem4a  32178  pj3lem1  32186  chrelat2i  32345  sumdmdii  32395  elim2if  32524  bnj1468  34858  bnj517  34897  acycgrislfgr  35196  axextdist  35841  funtransport  36073  bj-19.21t0  36872  bj-projval  37038  areacirc  37761  rngoueqz  37988  isdmn3  38122  ax12fromc15  38952  lkrlspeqN  39218  hlrelat2  39450  ps-1  39524  dalem54  39773  cdleme42c  40519  dihmeetlem6  41356  oe0suclim  43318  sdomne0  43454  sdomne0d  43455  frege124d  43802  uneqsn  44066  iotavalb  44471  natglobalincr  46923  2reuimp  47154  afv2orxorb  47267  iccpartnel  47477  fargshiftf1  47480  gbowge7  47802  sbgoldbwt  47816  bgoldbtbndlem1  47844  uspgrsprf1  48186  inisegn0a  48875