Theorem biimtrrdi 257

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 251	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ralnralall  4479  elinsn  4681  tppreqb  4777  sotri2  6130  sotri3  6131  somincom  6135  fnun  6650  fvmpti  6989  ovigg  7556  ndmovg  7594  onint  7788  tfindsg  7856  findsg  7893  resf1ext2b  7931  zfrep6OLD  7951  poxp2  8138  extmptsuppeq  8183  tfrlem9  8371  tfr3  8385  omlimcl  8562  oneo  8565  nnneo  8640  pssnn  9152  onomeneq  9197  inficl  9384  frmin  9720  updjud  9919  dfac2b  10113  axdc2lem  10431  axextnd  10575  canthp1lem2  10637  gchinf  10641  inatsk  10762  indpi  10891  ltaddpr2  11019  reclem2pr  11032  supsrlem  11095  axrrecex  11147  zeo  12681  nn0ind-raph  12695  fzm1  13634  fzind2  13816  addmodlteq  13981  bcpasc  14356  pr2pwpr  14515  swrdnnn0nd  14693  pwdif  15921  oddnn02np1  16405  oddge22np1  16406  evennn02n  16407  evennn2n  16408  bitsfzo  16492  bezoutlem1  16596  algcvgblem  16634  coprmdvds1  16709  qredeq  16714  prmreclem2  16976  ramtcl2  17070  divsfval  17600  joinval  18430  meetval  18444  gsumval3  19976  pgpfac1lem3a  20147  fiinopn  23026  restntr  23307  lly1stc  23621  dgradd2  26393  dgrcolem2  26399  asinneg  27016  ftalem2  27203  ftalem4  27205  ftalem5  27206  bpos1lem  27411  zabsle1  27425  lgsqrmodndvds  27482  incistruhgr  29369  fusgrfis  29620  uhgrnbgr0nb  29644  cusgrrusgr  29871  wlkswwlksf1o  30168  isclwwlknx  30327  clwwlknwwlksnb  30346  clwlknf1oclwwlknlem1  30372  frgrwopreglem3  30605  frgrreg  30685  frgrregord013  30686  h1de2ctlem  31847  pjclem4a  32490  pj3lem1  32498  chrelat2i  32657  sumdmdii  32707  elim2if  32830  bnj1468  35178  bnj517  35217  acycgrislfgr  35542  axextdist  36187  funtransport  36421  mh-setindnd  36936  bj-19.21t0  37353  bj-projval  37519  areacirc  38251  rngoueqz  38478  isdmn3  38612  ax12fromc15  39568  lkrlspeqN  39834  hlrelat2  40066  ps-1  40140  dalem54  40389  cdleme42c  41135  dihmeetlem6  41972  oe0suclim  43895  sdomne0  44030  sdomne0d  44031  frege124d  44378  uneqsn  44642  iotavalb  45031  natglobalincr  47484  2reuimp  47740  afv2orxorb  47853  iccpartnel  48075  fargshiftf1  48078  nprmdvdsfacm1lem2  48261  gbowge7  48416  sbgoldbwt  48430  bgoldbtbndlem1  48458  uspgrsprf1  48800  inisegn0a  49498