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  4538  elinsn  4735  tppreqb  4830  sotri2  6161  sotri3  6162  somincom  6166  fnun  6693  fvmpti  7028  ovigg  7595  ndmovg  7633  onint  7826  ordsucOLD  7850  tfindsg  7898  findsg  7937  zfrep6  7995  poxp2  8184  extmptsuppeq  8229  tfrlem9  8441  tfr3  8455  omlimcl  8634  oneo  8637  nnneo  8711  pssnn  9234  onomeneq  9291  inficl  9494  frmin  9818  updjud  10003  dfac2b  10200  axdc2lem  10517  axextnd  10660  canthp1lem2  10722  gchinf  10726  inatsk  10847  indpi  10976  ltaddpr2  11104  reclem2pr  11117  supsrlem  11180  axrrecex  11232  zeo  12729  nn0ind-raph  12743  fzm1  13664  fzind2  13835  addmodlteq  13997  bcpasc  14370  pr2pwpr  14528  swrdnnn0nd  14704  pwdif  15916  oddnn02np1  16396  oddge22np1  16397  evennn02n  16398  evennn2n  16399  bitsfzo  16481  bezoutlem1  16586  algcvgblem  16624  coprmdvds1  16699  qredeq  16704  prmreclem2  16964  ramtcl2  17058  divsfval  17607  joinval  18447  meetval  18461  gsumval3  19949  pgpfac1lem3a  20120  fiinopn  22928  restntr  23211  lly1stc  23525  dgradd2  26328  dgrcolem2  26334  asinneg  26947  ftalem2  27135  ftalem4  27137  ftalem5  27138  bpos1lem  27344  zabsle1  27358  lgsqrmodndvds  27415  incistruhgr  29114  fusgrfis  29365  uhgrnbgr0nb  29389  cusgrrusgr  29617  wlkswwlksf1o  29912  isclwwlknx  30068  clwwlknwwlksnb  30087  clwlknf1oclwwlknlem1  30113  frgrwopreglem3  30346  frgrreg  30426  frgrregord013  30427  h1de2ctlem  31587  pjclem4a  32230  pj3lem1  32238  chrelat2i  32397  sumdmdii  32447  elim2if  32567  bnj1468  34822  bnj517  34861  acycgrislfgr  35120  axextdist  35763  funtransport  35995  bj-19.21t0  36796  bj-projval  36962  areacirc  37673  rngoueqz  37900  isdmn3  38034  ax12fromc15  38861  lkrlspeqN  39127  hlrelat2  39360  ps-1  39434  dalem54  39683  cdleme42c  40429  dihmeetlem6  41266  oe0suclim  43239  sdomne0  43375  sdomne0d  43376  frege124d  43723  uneqsn  43987  iotavalb  44399  natglobalincr  46796  2reuimp  47030  afv2orxorb  47143  iccpartnel  47312  fargshiftf1  47315  gbowge7  47637  sbgoldbwt  47651  bgoldbtbndlem1  47679  uspgrsprf1  47870