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  4464  elinsn  4665  tppreqb  4759  sotri2  6084  sotri3  6085  somincom  6089  fnun  6604  fvmpti  6938  ovigg  7501  ndmovg  7539  onint  7733  tfindsg  7801  findsg  7837  resf1ext2b  7875  zfrep6  7897  poxp2  8083  extmptsuppeq  8128  tfrlem9  8314  tfr3  8328  omlimcl  8503  oneo  8506  nnneo  8581  pssnn  9091  onomeneq  9136  inficl  9326  frmin  9659  updjud  9844  dfac2b  10039  axdc2lem  10356  axextnd  10500  canthp1lem2  10562  gchinf  10566  inatsk  10687  indpi  10816  ltaddpr2  10944  reclem2pr  10957  supsrlem  11020  axrrecex  11072  zeo  12576  nn0ind-raph  12590  fzm1  13521  fzind2  13702  addmodlteq  13867  bcpasc  14242  pr2pwpr  14400  swrdnnn0nd  14578  pwdif  15789  oddnn02np1  16273  oddge22np1  16274  evennn02n  16275  evennn2n  16276  bitsfzo  16360  bezoutlem1  16464  algcvgblem  16502  coprmdvds1  16577  qredeq  16582  prmreclem2  16843  ramtcl2  16937  divsfval  17466  joinval  18296  meetval  18310  gsumval3  19834  pgpfac1lem3a  20005  fiinopn  22843  restntr  23124  lly1stc  23438  dgradd2  26228  dgrcolem2  26234  asinneg  26850  ftalem2  27038  ftalem4  27040  ftalem5  27041  bpos1lem  27247  zabsle1  27261  lgsqrmodndvds  27318  incistruhgr  29101  fusgrfis  29352  uhgrnbgr0nb  29376  cusgrrusgr  29604  wlkswwlksf1o  29901  isclwwlknx  30060  clwwlknwwlksnb  30079  clwlknf1oclwwlknlem1  30105  frgrwopreglem3  30338  frgrreg  30418  frgrregord013  30419  h1de2ctlem  31579  pjclem4a  32222  pj3lem1  32230  chrelat2i  32389  sumdmdii  32439  elim2if  32568  bnj1468  34951  bnj517  34990  acycgrislfgr  35295  axextdist  35940  funtransport  36174  bj-19.21t0  36974  bj-projval  37140  areacirc  37853  rngoueqz  38080  isdmn3  38214  ax12fromc15  39104  lkrlspeqN  39370  hlrelat2  39602  ps-1  39676  dalem54  39925  cdleme42c  40671  dihmeetlem6  41508  oe0suclim  43461  sdomne0  43596  sdomne0d  43597  frege124d  43944  uneqsn  44208  iotavalb  44613  natglobalincr  47063  2reuimp  47303  afv2orxorb  47416  iccpartnel  47626  fargshiftf1  47629  gbowge7  47951  sbgoldbwt  47965  bgoldbtbndlem1  47993  uspgrsprf1  48335  inisegn0a  49023