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  4453  elinsn  4654  tppreqb  4750  sotri2  6092  sotri3  6093  somincom  6097  fnun  6612  fvmpti  6946  ovigg  7512  ndmovg  7550  onint  7744  tfindsg  7812  findsg  7848  resf1ext2b  7886  zfrep6OLD  7908  poxp2  8093  extmptsuppeq  8138  tfrlem9  8324  tfr3  8338  omlimcl  8513  oneo  8516  nnneo  8591  pssnn  9103  onomeneq  9148  inficl  9338  frmin  9673  updjud  9858  dfac2b  10053  axdc2lem  10370  axextnd  10514  canthp1lem2  10576  gchinf  10580  inatsk  10701  indpi  10830  ltaddpr2  10958  reclem2pr  10971  supsrlem  11034  axrrecex  11086  zeo  12615  nn0ind-raph  12629  fzm1  13561  fzind2  13743  addmodlteq  13908  bcpasc  14283  pr2pwpr  14441  swrdnnn0nd  14619  pwdif  15833  oddnn02np1  16317  oddge22np1  16318  evennn02n  16319  evennn2n  16320  bitsfzo  16404  bezoutlem1  16508  algcvgblem  16546  coprmdvds1  16621  qredeq  16626  prmreclem2  16888  ramtcl2  16982  divsfval  17511  joinval  18341  meetval  18355  gsumval3  19882  pgpfac1lem3a  20053  fiinopn  22866  restntr  23147  lly1stc  23461  dgradd2  26233  dgrcolem2  26239  asinneg  26850  ftalem2  27037  ftalem4  27039  ftalem5  27040  bpos1lem  27245  zabsle1  27259  lgsqrmodndvds  27316  incistruhgr  29148  fusgrfis  29399  uhgrnbgr0nb  29423  cusgrrusgr  29650  wlkswwlksf1o  29947  isclwwlknx  30106  clwwlknwwlksnb  30125  clwlknf1oclwwlknlem1  30151  frgrwopreglem3  30384  frgrreg  30464  frgrregord013  30465  h1de2ctlem  31626  pjclem4a  32269  pj3lem1  32277  chrelat2i  32436  sumdmdii  32486  elim2if  32614  bnj1468  34988  bnj517  35027  acycgrislfgr  35334  axextdist  35979  funtransport  36213  mh-setindnd  36719  bj-19.21t0  37137  bj-projval  37303  areacirc  38034  rngoueqz  38261  isdmn3  38395  ax12fromc15  39351  lkrlspeqN  39617  hlrelat2  39849  ps-1  39923  dalem54  40172  cdleme42c  40918  dihmeetlem6  41755  oe0suclim  43705  sdomne0  43840  sdomne0d  43841  frege124d  44188  uneqsn  44452  iotavalb  44857  natglobalincr  47307  2reuimp  47563  afv2orxorb  47676  iccpartnel  47898  fargshiftf1  47901  nprmdvdsfacm1lem2  48084  gbowge7  48239  sbgoldbwt  48253  bgoldbtbndlem1  48281  uspgrsprf1  48623  inisegn0a  49311