Theorem biimtrrdi 253

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 247	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		biimtrrdi.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ralnralall  4523  elinsn  4719  tppreqb  4814  sotri2  6141  sotri3  6142  somincom  6146  fnun  6674  fvmpti  7008  ovigg  7571  ndmovg  7609  onint  7799  ordsucOLD  7823  tfindsg  7871  findsg  7910  zfrep6  7968  poxp2  8157  extmptsuppeq  8202  tfrlem9  8415  tfr3  8429  omlimcl  8608  oneo  8611  nnneo  8685  pssnn  9206  onomeneq  9262  pssnnOLD  9299  inficl  9468  frmin  9792  updjud  9977  dfac2b  10173  axdc2lem  10491  axextnd  10634  canthp1lem2  10696  gchinf  10700  inatsk  10821  indpi  10950  ltaddpr2  11078  reclem2pr  11091  supsrlem  11154  axrrecex  11206  zeo  12700  nn0ind-raph  12714  fzm1  13635  fzind2  13805  addmodlteq  13966  bcpasc  14338  pr2pwpr  14498  swrdnnn0nd  14664  pwdif  15872  oddnn02np1  16350  oddge22np1  16351  evennn02n  16352  evennn2n  16353  bitsfzo  16435  bezoutlem1  16540  algcvgblem  16578  coprmdvds1  16653  qredeq  16658  prmreclem2  16919  ramtcl2  17013  divsfval  17562  joinval  18402  meetval  18416  gsumval3  19905  pgpfac1lem3a  20076  fiinopn  22894  restntr  23177  lly1stc  23491  dgradd2  26296  dgrcolem2  26302  asinneg  26914  ftalem2  27102  ftalem4  27104  ftalem5  27105  bpos1lem  27311  zabsle1  27325  lgsqrmodndvds  27382  incistruhgr  29015  fusgrfis  29266  uhgrnbgr0nb  29290  cusgrrusgr  29518  wlkswwlksf1o  29813  isclwwlknx  29969  clwwlknwwlksnb  29988  clwlknf1oclwwlknlem1  30014  frgrwopreglem3  30247  frgrreg  30327  frgrregord013  30328  h1de2ctlem  31488  pjclem4a  32131  pj3lem1  32139  chrelat2i  32298  sumdmdii  32348  elim2if  32465  bnj1468  34691  bnj517  34730  acycgrislfgr  34980  axextdist  35623  funtransport  35855  bj-19.21t0  36535  bj-projval  36703  areacirc  37414  rngoueqz  37641  isdmn3  37775  ax12fromc15  38603  lkrlspeqN  38869  hlrelat2  39102  ps-1  39176  dalem54  39425  cdleme42c  40171  dihmeetlem6  41008  oe0suclim  42943  sdomne0  43080  sdomne0d  43081  frege124d  43428  uneqsn  43692  iotavalb  44104  natglobalincr  46496  2reuimp  46728  afv2orxorb  46841  iccpartnel  47010  fargshiftf1  47013  gbowge7  47335  sbgoldbwt  47349  bgoldbtbndlem1  47377  uspgrsprf1  47524