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  4495  elinsn  4691  tppreqb  4786  sotri2  6123  sotri3  6124  somincom  6128  fnun  6657  fvmpti  6990  ovigg  7557  ndmovg  7595  onint  7789  ordsucOLD  7813  tfindsg  7861  findsg  7898  resf1ext2b  7936  zfrep6  7958  poxp2  8147  extmptsuppeq  8192  tfrlem9  8404  tfr3  8418  omlimcl  8595  oneo  8598  nnneo  8672  pssnn  9187  onomeneq  9242  inficl  9442  frmin  9768  updjud  9953  dfac2b  10150  axdc2lem  10467  axextnd  10610  canthp1lem2  10672  gchinf  10676  inatsk  10797  indpi  10926  ltaddpr2  11054  reclem2pr  11067  supsrlem  11130  axrrecex  11182  zeo  12684  nn0ind-raph  12698  fzm1  13629  fzind2  13806  addmodlteq  13969  bcpasc  14344  pr2pwpr  14502  swrdnnn0nd  14679  pwdif  15889  oddnn02np1  16372  oddge22np1  16373  evennn02n  16374  evennn2n  16375  bitsfzo  16459  bezoutlem1  16563  algcvgblem  16601  coprmdvds1  16676  qredeq  16681  prmreclem2  16942  ramtcl2  17036  divsfval  17566  joinval  18392  meetval  18406  gsumval3  19893  pgpfac1lem3a  20064  fiinopn  22844  restntr  23125  lly1stc  23439  dgradd2  26231  dgrcolem2  26237  asinneg  26853  ftalem2  27041  ftalem4  27043  ftalem5  27044  bpos1lem  27250  zabsle1  27264  lgsqrmodndvds  27321  incistruhgr  29063  fusgrfis  29314  uhgrnbgr0nb  29338  cusgrrusgr  29566  wlkswwlksf1o  29866  isclwwlknx  30022  clwwlknwwlksnb  30041  clwlknf1oclwwlknlem1  30067  frgrwopreglem3  30300  frgrreg  30380  frgrregord013  30381  h1de2ctlem  31541  pjclem4a  32184  pj3lem1  32192  chrelat2i  32351  sumdmdii  32401  elim2if  32530  bnj1468  34882  bnj517  34921  acycgrislfgr  35179  axextdist  35822  funtransport  36054  bj-19.21t0  36853  bj-projval  37019  areacirc  37742  rngoueqz  37969  isdmn3  38103  ax12fromc15  38928  lkrlspeqN  39194  hlrelat2  39427  ps-1  39501  dalem54  39750  cdleme42c  40496  dihmeetlem6  41333  oe0suclim  43268  sdomne0  43404  sdomne0d  43405  frege124d  43752  uneqsn  44016  iotavalb  44421  natglobalincr  46873  2reuimp  47111  afv2orxorb  47224  iccpartnel  47419  fargshiftf1  47422  gbowge7  47744  sbgoldbwt  47758  bgoldbtbndlem1  47786  uspgrsprf1  48089  inisegn0a  48781