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  4454  elinsn  4655  tppreqb  4749  sotri2  6087  sotri3  6088  somincom  6092  fnun  6607  fvmpti  6941  ovigg  7506  ndmovg  7544  onint  7738  tfindsg  7806  findsg  7842  resf1ext2b  7880  zfrep6OLD  7902  poxp2  8087  extmptsuppeq  8132  tfrlem9  8318  tfr3  8332  omlimcl  8507  oneo  8510  nnneo  8585  pssnn  9097  onomeneq  9142  inficl  9332  frmin  9667  updjud  9852  dfac2b  10047  axdc2lem  10364  axextnd  10508  canthp1lem2  10570  gchinf  10574  inatsk  10695  indpi  10824  ltaddpr2  10952  reclem2pr  10965  supsrlem  11028  axrrecex  11080  zeo  12609  nn0ind-raph  12623  fzm1  13555  fzind2  13737  addmodlteq  13902  bcpasc  14277  pr2pwpr  14435  swrdnnn0nd  14613  pwdif  15827  oddnn02np1  16311  oddge22np1  16312  evennn02n  16313  evennn2n  16314  bitsfzo  16398  bezoutlem1  16502  algcvgblem  16540  coprmdvds1  16615  qredeq  16620  prmreclem2  16882  ramtcl2  16976  divsfval  17505  joinval  18335  meetval  18349  gsumval3  19876  pgpfac1lem3a  20047  fiinopn  22879  restntr  23160  lly1stc  23474  dgradd2  26246  dgrcolem2  26252  asinneg  26866  ftalem2  27054  ftalem4  27056  ftalem5  27057  bpos1lem  27262  zabsle1  27276  lgsqrmodndvds  27333  incistruhgr  29165  fusgrfis  29416  uhgrnbgr0nb  29440  cusgrrusgr  29668  wlkswwlksf1o  29965  isclwwlknx  30124  clwwlknwwlksnb  30143  clwlknf1oclwwlknlem1  30169  frgrwopreglem3  30402  frgrreg  30482  frgrregord013  30483  h1de2ctlem  31644  pjclem4a  32287  pj3lem1  32295  chrelat2i  32454  sumdmdii  32504  elim2if  32632  bnj1468  35007  bnj517  35046  acycgrislfgr  35353  axextdist  35998  funtransport  36232  mh-setindnd  36738  bj-19.21t0  37156  bj-projval  37322  areacirc  38051  rngoueqz  38278  isdmn3  38412  ax12fromc15  39368  lkrlspeqN  39634  hlrelat2  39866  ps-1  39940  dalem54  40189  cdleme42c  40935  dihmeetlem6  41772  oe0suclim  43726  sdomne0  43861  sdomne0d  43862  frege124d  44209  uneqsn  44473  iotavalb  44878  natglobalincr  47326  2reuimp  47578  afv2orxorb  47691  iccpartnel  47913  fargshiftf1  47916  nprmdvdsfacm1lem2  48099  gbowge7  48254  sbgoldbwt  48268  bgoldbtbndlem1  48296  uspgrsprf1  48638  inisegn0a  49326