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  4481  elinsn  4677  tppreqb  4772  sotri2  6105  sotri3  6106  somincom  6110  fnun  6635  fvmpti  6970  ovigg  7537  ndmovg  7575  onint  7769  ordsucOLD  7792  tfindsg  7840  findsg  7876  resf1ext2b  7914  zfrep6  7936  poxp2  8125  extmptsuppeq  8170  tfrlem9  8356  tfr3  8370  omlimcl  8545  oneo  8548  nnneo  8622  pssnn  9138  onomeneq  9184  inficl  9383  frmin  9709  updjud  9894  dfac2b  10091  axdc2lem  10408  axextnd  10551  canthp1lem2  10613  gchinf  10617  inatsk  10738  indpi  10867  ltaddpr2  10995  reclem2pr  11008  supsrlem  11071  axrrecex  11123  zeo  12627  nn0ind-raph  12641  fzm1  13575  fzind2  13753  addmodlteq  13918  bcpasc  14293  pr2pwpr  14451  swrdnnn0nd  14628  pwdif  15841  oddnn02np1  16325  oddge22np1  16326  evennn02n  16327  evennn2n  16328  bitsfzo  16412  bezoutlem1  16516  algcvgblem  16554  coprmdvds1  16629  qredeq  16634  prmreclem2  16895  ramtcl2  16989  divsfval  17517  joinval  18343  meetval  18357  gsumval3  19844  pgpfac1lem3a  20015  fiinopn  22795  restntr  23076  lly1stc  23390  dgradd2  26181  dgrcolem2  26187  asinneg  26803  ftalem2  26991  ftalem4  26993  ftalem5  26994  bpos1lem  27200  zabsle1  27214  lgsqrmodndvds  27271  incistruhgr  29013  fusgrfis  29264  uhgrnbgr0nb  29288  cusgrrusgr  29516  wlkswwlksf1o  29816  isclwwlknx  29972  clwwlknwwlksnb  29991  clwlknf1oclwwlknlem1  30017  frgrwopreglem3  30250  frgrreg  30330  frgrregord013  30331  h1de2ctlem  31491  pjclem4a  32134  pj3lem1  32142  chrelat2i  32301  sumdmdii  32351  elim2if  32480  bnj1468  34843  bnj517  34882  acycgrislfgr  35146  axextdist  35794  funtransport  36026  bj-19.21t0  36825  bj-projval  36991  areacirc  37714  rngoueqz  37941  isdmn3  38075  ax12fromc15  38905  lkrlspeqN  39171  hlrelat2  39404  ps-1  39478  dalem54  39727  cdleme42c  40473  dihmeetlem6  41310  oe0suclim  43273  sdomne0  43409  sdomne0d  43410  frege124d  43757  uneqsn  44021  iotavalb  44426  natglobalincr  46882  2reuimp  47120  afv2orxorb  47233  iccpartnel  47443  fargshiftf1  47446  gbowge7  47768  sbgoldbwt  47782  bgoldbtbndlem1  47810  uspgrsprf1  48139  inisegn0a  48828