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  4466  elinsn  4667  tppreqb  4761  sotri2  6086  sotri3  6087  somincom  6091  fnun  6606  fvmpti  6940  ovigg  7503  ndmovg  7541  onint  7735  tfindsg  7803  findsg  7839  resf1ext2b  7877  zfrep6  7899  poxp2  8085  extmptsuppeq  8130  tfrlem9  8316  tfr3  8330  omlimcl  8505  oneo  8508  nnneo  8583  pssnn  9093  onomeneq  9138  inficl  9328  frmin  9661  updjud  9846  dfac2b  10041  axdc2lem  10358  axextnd  10502  canthp1lem2  10564  gchinf  10568  inatsk  10689  indpi  10818  ltaddpr2  10946  reclem2pr  10959  supsrlem  11022  axrrecex  11074  zeo  12578  nn0ind-raph  12592  fzm1  13523  fzind2  13704  addmodlteq  13869  bcpasc  14244  pr2pwpr  14402  swrdnnn0nd  14580  pwdif  15791  oddnn02np1  16275  oddge22np1  16276  evennn02n  16277  evennn2n  16278  bitsfzo  16362  bezoutlem1  16466  algcvgblem  16504  coprmdvds1  16579  qredeq  16584  prmreclem2  16845  ramtcl2  16939  divsfval  17468  joinval  18298  meetval  18312  gsumval3  19836  pgpfac1lem3a  20007  fiinopn  22845  restntr  23126  lly1stc  23440  dgradd2  26230  dgrcolem2  26236  asinneg  26852  ftalem2  27040  ftalem4  27042  ftalem5  27043  bpos1lem  27249  zabsle1  27263  lgsqrmodndvds  27320  incistruhgr  29152  fusgrfis  29403  uhgrnbgr0nb  29427  cusgrrusgr  29655  wlkswwlksf1o  29952  isclwwlknx  30111  clwwlknwwlksnb  30130  clwlknf1oclwwlknlem1  30156  frgrwopreglem3  30389  frgrreg  30469  frgrregord013  30470  h1de2ctlem  31630  pjclem4a  32273  pj3lem1  32281  chrelat2i  32440  sumdmdii  32490  elim2if  32619  bnj1468  35002  bnj517  35041  acycgrislfgr  35346  axextdist  35991  funtransport  36225  mh-setindnd  36667  bj-19.21t0  37031  bj-projval  37197  areacirc  37914  rngoueqz  38141  isdmn3  38275  ax12fromc15  39165  lkrlspeqN  39431  hlrelat2  39663  ps-1  39737  dalem54  39986  cdleme42c  40732  dihmeetlem6  41569  oe0suclim  43519  sdomne0  43654  sdomne0d  43655  frege124d  44002  uneqsn  44266  iotavalb  44671  natglobalincr  47121  2reuimp  47361  afv2orxorb  47474  iccpartnel  47684  fargshiftf1  47687  gbowge7  48009  sbgoldbwt  48023  bgoldbtbndlem1  48051  uspgrsprf1  48393  inisegn0a  49081