Theorem biimtrrdi 257

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ralnralall  4474  elinsn  4676  tppreqb  4773  sotri2  6129  sotri3  6130  somincom  6134  fnun  6649  fvmpti  6988  ovigg  7555  ndmovg  7593  onint  7785  tfindsg  7853  findsg  7890  resf1ext2b  7928  zfrep6OLD  7948  poxp2  8135  extmptsuppeq  8180  tfrlem9  8368  tfr3  8382  omlimcl  8559  oneo  8562  nnneo  8637  pssnn  9149  onomeneq  9194  inficl  9381  frmin  9717  updjud  9916  dfac2b  10110  axdc2lem  10427  axextnd  10571  canthp1lem2  10633  gchinf  10637  inatsk  10758  indpi  10887  ltaddpr2  11015  reclem2pr  11028  supsrlem  11091  axrrecex  11143  zeo  12677  nn0ind-raph  12691  fzm1  13631  fzind2  13813  addmodlteq  13978  bcpasc  14353  pr2pwpr  14512  swrdnnn0nd  14690  pwdif  15918  oddnn02np1  16401  oddge22np1  16402  evennn02n  16403  evennn2n  16404  bitsfzo  16488  bezoutlem1  16592  algcvgblem  16630  coprmdvds1  16705  qredeq  16710  prmreclem2  16972  ramtcl2  17066  divsfval  17596  joinval  18426  meetval  18440  gsumval3  19972  pgpfac1lem3a  20143  fiinopn  23058  restntr  23339  lly1stc  23653  dgradd2  26425  dgrcolem2  26431  asinneg  27051  ftalem2  27238  ftalem4  27240  ftalem5  27241  bpos1lem  27446  zabsle1  27460  lgsqrmodndvds  27517  incistruhgr  29429  fusgrfis  29680  uhgrnbgr0nb  29704  cusgrrusgr  29931  wlkswwlksf1o  30228  isclwwlknx  30387  clwwlknwwlksnb  30406  clwlknf1oclwwlknlem1  30432  frgrwopreglem3  30665  frgrreg  30745  frgrregord013  30746  h1de2ctlem  31907  pjclem4a  32550  pj3lem1  32558  chrelat2i  32717  sumdmdii  32767  elim2if  32890  bnj1468  35234  bnj517  35273  acycgrislfgr  35644  axextdist  36289  funtransport  36523  mh-setindnd  37048  bj-19.21t0  37465  bj-projval  37632  areacirc  38364  rngoueqz  38591  isdmn3  38725  ax12fromc15  39679  lkrlspeqN  39945  hlrelat2  40177  ps-1  40251  dalem54  40500  cdleme42c  41246  dihmeetlem6  42083  oe0suclim  44004  sdomne0  44139  sdomne0d  44140  frege124d  44487  uneqsn  44751  iotavalb  45140  natglobalincr  47593  2reuimp  47852  afv2orxorb  47965  iccpartnel  48187  fargshiftf1  48190  nprmdvdsfacm1lem2  48373  gbowge7  48528  sbgoldbwt  48542  bgoldbtbndlem1  48570  uspgrsprf1  48912  isidom3  49110  inisegn0a  49614