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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ralnralall  4469  elinsn  4671  tppreqb  4768  sotri2  6123  sotri3  6124  somincom  6128  fnun  6646  fvmpti  6985  ovigg  7558  ndmovg  7597  onint  7789  tfindsg  7857  findsg  7894  resf1ext2b  7932  zfrep6OLD  7952  poxp2  8141  extmptsuppeq  8186  tfrlem9  8374  tfr3  8388  omlimcl  8565  oneo  8568  nnneo  8643  pssnn  9163  onomeneq  9208  inficl  9395  frmin  9731  updjud  9939  dfac2b  10133  axdc2lem  10450  axextnd  10600  canthp1lem2  10662  gchinf  10666  inatsk  10787  indpi  10916  ltaddpr2  11044  reclem2pr  11057  supsrlem  11120  axrrecex  11172  zeo  12707  nn0ind-raph  12721  fzm1  13662  fzind2  13844  addmodlteq  14010  bcpasc  14385  pr2pwpr  14544  swrdnnn0nd  14726  pwdif  15957  oddnn02np1  16438  oddge22np1  16439  evennn02n  16440  evennn2n  16441  bitsfzo  16525  bezoutlem1  16629  algcvgblem  16667  coprmdvds1  16742  qredeq  16747  prmreclem2  17009  ramtcl2  17103  divsfval  17633  joinval  18463  meetval  18477  gsumval3  20034  pgpfac1lem3a  20205  fiinopn  23126  restntr  23407  lly1stc  23722  dgradd2  26494  dgrcolem2  26500  asinneg  27123  ftalem2  27310  ftalem4  27312  ftalem5  27313  bpos1lem  27518  zabsle1  27532  lgsqrmodndvds  27589  incistruhgr  29536  fusgrfis  29790  uhgrnbgr0nb  29814  cusgrrusgr  30041  wlkswwlksf1o  30347  isclwwlknx  30506  clwwlknwwlksnb  30525  clwlknf1oclwwlknlem1  30551  frgrwopreglem3  30794  frgrreg  30874  frgrregord013  30875  h1de2ctlem  32036  pjclem4a  32679  pj3lem1  32687  chrelat2i  32846  sumdmdii  32896  elim2if  33019  bnj1468  35355  bnj517  35394  acycgrislfgr  35731  axextdist  36376  funtransport  36611  mh-setindnd  37156  bj-19.21t0  37573  bj-projval  37740  areacirc  38462  rngoueqz  38690  isdmn3  38824  ax12fromc15  39778  lkrlspeqN  40044  hlrelat2  40276  ps-1  40350  dalem54  40599  cdleme42c  41345  dihmeetlem6  42182  oe0suclim  44118  sdomne0  44253  sdomne0d  44254  frege124d  44601  uneqsn  44865  iotavalb  45254  2reuimp  48003  afv2orxorb  48116  iccpartnel  48338  fargshiftf1  48341  nprmdvdsfacm1lem2  48524  gbowge7  48679  sbgoldbwt  48693  bgoldbtbndlem1  48721  uspgrsprf1  49063  isidom3  49260  inisegn0a  49764