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  4521  elinsn  4715  tppreqb  4810  sotri2  6152  sotri3  6153  somincom  6157  fnun  6683  fvmpti  7015  ovigg  7578  ndmovg  7616  onint  7810  ordsucOLD  7834  tfindsg  7882  findsg  7920  zfrep6  7978  poxp2  8167  extmptsuppeq  8212  tfrlem9  8424  tfr3  8438  omlimcl  8615  oneo  8618  nnneo  8692  pssnn  9207  onomeneq  9263  inficl  9463  frmin  9787  updjud  9972  dfac2b  10169  axdc2lem  10486  axextnd  10629  canthp1lem2  10691  gchinf  10695  inatsk  10816  indpi  10945  ltaddpr2  11073  reclem2pr  11086  supsrlem  11149  axrrecex  11201  zeo  12702  nn0ind-raph  12716  fzm1  13644  fzind2  13821  addmodlteq  13984  bcpasc  14357  pr2pwpr  14515  swrdnnn0nd  14691  pwdif  15901  oddnn02np1  16382  oddge22np1  16383  evennn02n  16384  evennn2n  16385  bitsfzo  16469  bezoutlem1  16573  algcvgblem  16611  coprmdvds1  16686  qredeq  16691  prmreclem2  16951  ramtcl2  17045  divsfval  17594  joinval  18435  meetval  18449  gsumval3  19940  pgpfac1lem3a  20111  fiinopn  22923  restntr  23206  lly1stc  23520  dgradd2  26323  dgrcolem2  26329  asinneg  26944  ftalem2  27132  ftalem4  27134  ftalem5  27135  bpos1lem  27341  zabsle1  27355  lgsqrmodndvds  27412  incistruhgr  29111  fusgrfis  29362  uhgrnbgr0nb  29386  cusgrrusgr  29614  wlkswwlksf1o  29909  isclwwlknx  30065  clwwlknwwlksnb  30084  clwlknf1oclwwlknlem1  30110  frgrwopreglem3  30343  frgrreg  30423  frgrregord013  30424  h1de2ctlem  31584  pjclem4a  32227  pj3lem1  32235  chrelat2i  32394  sumdmdii  32444  elim2if  32565  bnj1468  34839  bnj517  34878  acycgrislfgr  35137  axextdist  35781  funtransport  36013  bj-19.21t0  36813  bj-projval  36979  areacirc  37700  rngoueqz  37927  isdmn3  38061  ax12fromc15  38887  lkrlspeqN  39153  hlrelat2  39386  ps-1  39460  dalem54  39709  cdleme42c  40455  dihmeetlem6  41292  oe0suclim  43267  sdomne0  43403  sdomne0d  43404  frege124d  43751  uneqsn  44015  iotavalb  44426  natglobalincr  46831  2reuimp  47065  afv2orxorb  47178  iccpartnel  47363  fargshiftf1  47366  gbowge7  47688  sbgoldbwt  47702  bgoldbtbndlem1  47730  uspgrsprf1  47991