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  4468  elinsn  4667  tppreqb  4764  sotri2  6125  sotri3  6126  somincom  6130  fnun  6658  fvmpti  6997  ovigg  7569  ndmovg  7608  onint  7808  tfindsg  7876  findsg  7913  resf1ext2b  7951  zfrep6OLD  7971  poxp2  8166  extmptsuppeq  8212  tfrlem9  8400  tfr3  8414  omlimcl  8593  oneo  8596  nnneo  8671  pssnn  9191  onomeneq  9236  inficl  9424  frmin  9760  updjud  10022  dfac2b  10216  axdc2lem  10533  axextnd  10683  canthp1lem2  10745  gchinf  10749  inatsk  10870  indpi  10999  ltaddpr2  11127  reclem2pr  11140  supsrlem  11203  axrrecex  11255  zeo  12792  nn0ind-raph  12806  fzm1  13748  fzind2  13930  addmodlteq  14096  bcpasc  14472  pr2pwpr  14631  swrdnnn0nd  14814  pwdif  16046  oddnn02np1  16527  oddge22np1  16528  evennn02n  16529  evennn2n  16530  bitsfzo  16614  bezoutlem1  16721  algcvgblem  16761  coprmdvds1  16836  qredeq  16841  prmreclem2  17104  ramtcl2  17198  divsfval  17728  joinval  18558  meetval  18572  gsumval3  20130  pgpfac1lem3a  20301  fiinopn  23228  restntr  23509  lly1stc  23824  dgradd2  26596  dgrcolem2  26602  asinneg  27223  ftalem2  27410  ftalem4  27412  ftalem5  27413  bpos1lem  27618  zabsle1  27632  lgsqrmodndvds  27689  incistruhgr  29666  fusgrfis  29920  uhgrnbgr0nb  29944  cusgrrusgr  30171  wlkswwlksf1o  30477  isclwwlknx  30636  clwwlknwwlksnb  30655  clwlknf1oclwwlknlem1  30681  frgrwopreglem3  30924  frgrreg  31004  frgrregord013  31005  h1de2ctlem  32166  pjclem4a  32809  pj3lem1  32817  chrelat2i  32976  sumdmdii  33026  elim2if  33191  bnj1468  35526  bnj517  35565  acycgrislfgr  35997  axextdist  36657  funtransport  36892  mh-setindnd  37421  bj-19.21t0  37838  bj-projval  38005  areacirc  38740  rngoueqz  38983  isdmn3  39117  ax12fromc15  40071  lkrlspeqN  40337  hlrelat2  40569  ps-1  40643  dalem54  40892  cdleme42c  41638  dihmeetlem6  42475  oe0suclim  44388  sdomne0  44523  sdomne0d  44524  frege124d  44870  uneqsn  45134  iotavalb  45522  2reuimp  48294  afv2orxorb  48406  iccpartnel  48628  fargshiftf1  48631  nprmdvdsfacm1lem2  48814  gbowge7  48969  sbgoldbwt  48983  bgoldbtbndlem1  49011  uspgrsprf1  49353  isidom3  49550  inisegn0a  50055