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  4474  elinsn  4670  tppreqb  4765  sotri2  6090  sotri3  6091  somincom  6095  fnun  6614  fvmpti  6949  ovigg  7514  ndmovg  7552  onint  7746  ordsucOLD  7769  tfindsg  7817  findsg  7853  resf1ext2b  7891  zfrep6  7913  poxp2  8099  extmptsuppeq  8144  tfrlem9  8330  tfr3  8344  omlimcl  8519  oneo  8522  nnneo  8596  pssnn  9109  onomeneq  9155  inficl  9352  frmin  9678  updjud  9863  dfac2b  10060  axdc2lem  10377  axextnd  10520  canthp1lem2  10582  gchinf  10586  inatsk  10707  indpi  10836  ltaddpr2  10964  reclem2pr  10977  supsrlem  11040  axrrecex  11092  zeo  12596  nn0ind-raph  12610  fzm1  13544  fzind2  13722  addmodlteq  13887  bcpasc  14262  pr2pwpr  14420  swrdnnn0nd  14597  pwdif  15810  oddnn02np1  16294  oddge22np1  16295  evennn02n  16296  evennn2n  16297  bitsfzo  16381  bezoutlem1  16485  algcvgblem  16523  coprmdvds1  16598  qredeq  16603  prmreclem2  16864  ramtcl2  16958  divsfval  17486  joinval  18316  meetval  18330  gsumval3  19821  pgpfac1lem3a  19992  fiinopn  22821  restntr  23102  lly1stc  23416  dgradd2  26207  dgrcolem2  26213  asinneg  26829  ftalem2  27017  ftalem4  27019  ftalem5  27020  bpos1lem  27226  zabsle1  27240  lgsqrmodndvds  27297  incistruhgr  29059  fusgrfis  29310  uhgrnbgr0nb  29334  cusgrrusgr  29562  wlkswwlksf1o  29859  isclwwlknx  30015  clwwlknwwlksnb  30034  clwlknf1oclwwlknlem1  30060  frgrwopreglem3  30293  frgrreg  30373  frgrregord013  30374  h1de2ctlem  31534  pjclem4a  32177  pj3lem1  32185  chrelat2i  32344  sumdmdii  32394  elim2if  32523  bnj1468  34829  bnj517  34868  acycgrislfgr  35132  axextdist  35780  funtransport  36012  bj-19.21t0  36811  bj-projval  36977  areacirc  37700  rngoueqz  37927  isdmn3  38061  ax12fromc15  38891  lkrlspeqN  39157  hlrelat2  39390  ps-1  39464  dalem54  39713  cdleme42c  40459  dihmeetlem6  41296  oe0suclim  43259  sdomne0  43395  sdomne0d  43396  frege124d  43743  uneqsn  44007  iotavalb  44412  natglobalincr  46868  2reuimp  47109  afv2orxorb  47222  iccpartnel  47432  fargshiftf1  47435  gbowge7  47757  sbgoldbwt  47771  bgoldbtbndlem1  47799  uspgrsprf1  48128  inisegn0a  48817