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  4468  elinsn  4669  tppreqb  4763  sotri2  6094  sotri3  6095  somincom  6099  fnun  6614  fvmpti  6948  ovigg  7513  ndmovg  7551  onint  7745  tfindsg  7813  findsg  7849  resf1ext2b  7887  zfrep6  7909  poxp2  8095  extmptsuppeq  8140  tfrlem9  8326  tfr3  8340  omlimcl  8515  oneo  8518  nnneo  8593  pssnn  9105  onomeneq  9150  inficl  9340  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  12590  nn0ind-raph  12604  fzm1  13535  fzind2  13716  addmodlteq  13881  bcpasc  14256  pr2pwpr  14414  swrdnnn0nd  14592  pwdif  15803  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  bitsfzo  16374  bezoutlem1  16478  algcvgblem  16516  coprmdvds1  16591  qredeq  16596  prmreclem2  16857  ramtcl2  16951  divsfval  17480  joinval  18310  meetval  18324  gsumval3  19848  pgpfac1lem3a  20019  fiinopn  22857  restntr  23138  lly1stc  23452  dgradd2  26242  dgrcolem2  26248  asinneg  26864  ftalem2  27052  ftalem4  27054  ftalem5  27055  bpos1lem  27261  zabsle1  27275  lgsqrmodndvds  27332  incistruhgr  29164  fusgrfis  29415  uhgrnbgr0nb  29439  cusgrrusgr  29667  wlkswwlksf1o  29964  isclwwlknx  30123  clwwlknwwlksnb  30142  clwlknf1oclwwlknlem1  30168  frgrwopreglem3  30401  frgrreg  30481  frgrregord013  30482  h1de2ctlem  31643  pjclem4a  32286  pj3lem1  32294  chrelat2i  32453  sumdmdii  32503  elim2if  32631  bnj1468  35022  bnj517  35061  acycgrislfgr  35368  axextdist  36013  funtransport  36247  mh-setindnd  36689  bj-19.21t0  37078  bj-projval  37244  areacirc  37964  rngoueqz  38191  isdmn3  38325  ax12fromc15  39281  lkrlspeqN  39547  hlrelat2  39779  ps-1  39853  dalem54  40102  cdleme42c  40848  dihmeetlem6  41685  oe0suclim  43634  sdomne0  43769  sdomne0d  43770  frege124d  44117  uneqsn  44381  iotavalb  44786  natglobalincr  47235  2reuimp  47475  afv2orxorb  47588  iccpartnel  47798  fargshiftf1  47801  gbowge7  48123  sbgoldbwt  48137  bgoldbtbndlem1  48165  uspgrsprf1  48507  inisegn0a  49195