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  4476  elinsn  4678  tppreqb  4775  sotri2  6131  sotri3  6132  somincom  6136  fnun  6653  fvmpti  6992  ovigg  7564  ndmovg  7603  onint  7795  tfindsg  7863  findsg  7900  resf1ext2b  7938  zfrep6OLD  7958  poxp2  8145  extmptsuppeq  8190  tfrlem9  8378  tfr3  8392  omlimcl  8569  oneo  8572  nnneo  8647  pssnn  9160  onomeneq  9205  inficl  9392  frmin  9728  updjud  9936  dfac2b  10130  axdc2lem  10447  axextnd  10591  canthp1lem2  10653  gchinf  10657  inatsk  10778  indpi  10907  ltaddpr2  11035  reclem2pr  11048  supsrlem  11111  axrrecex  11163  zeo  12698  nn0ind-raph  12712  fzm1  13652  fzind2  13834  addmodlteq  14000  bcpasc  14375  pr2pwpr  14534  swrdnnn0nd  14716  pwdif  15945  oddnn02np1  16428  oddge22np1  16429  evennn02n  16430  evennn2n  16431  bitsfzo  16515  bezoutlem1  16619  algcvgblem  16657  coprmdvds1  16732  qredeq  16737  prmreclem2  16999  ramtcl2  17093  divsfval  17623  joinval  18453  meetval  18467  gsumval3  20021  pgpfac1lem3a  20192  fiinopn  23108  restntr  23389  lly1stc  23704  dgradd2  26476  dgrcolem2  26482  asinneg  27102  ftalem2  27289  ftalem4  27291  ftalem5  27292  bpos1lem  27497  zabsle1  27511  lgsqrmodndvds  27568  incistruhgr  29484  fusgrfis  29738  uhgrnbgr0nb  29762  cusgrrusgr  29989  wlkswwlksf1o  30295  isclwwlknx  30454  clwwlknwwlksnb  30473  clwlknf1oclwwlknlem1  30499  frgrwopreglem3  30736  frgrreg  30816  frgrregord013  30817  h1de2ctlem  31978  pjclem4a  32621  pj3lem1  32629  chrelat2i  32788  sumdmdii  32838  elim2if  32961  bnj1468  35299  bnj517  35338  acycgrislfgr  35681  axextdist  36326  funtransport  36560  mh-setindnd  37105  bj-19.21t0  37522  bj-projval  37689  areacirc  38421  rngoueqz  38649  isdmn3  38783  ax12fromc15  39737  lkrlspeqN  40003  hlrelat2  40235  ps-1  40309  dalem54  40558  cdleme42c  41304  dihmeetlem6  42141  oe0suclim  44062  sdomne0  44197  sdomne0d  44198  frege124d  44545  uneqsn  44809  iotavalb  45198  natglobalincr  47651  2reuimp  47910  afv2orxorb  48023  iccpartnel  48245  fargshiftf1  48248  nprmdvdsfacm1lem2  48431  gbowge7  48586  sbgoldbwt  48600  bgoldbtbndlem1  48628  uspgrsprf1  48970  isidom3  49167  inisegn0a  49671