Theorem imbitrid 244

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
imbitrid.1	⊢ (𝜑 → 𝜓)
imbitrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem imbitrid

Step	Hyp	Ref	Expression
1		imbitrid.1	. 2 ⊢ (𝜑 → 𝜓)
2		imbitrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 229	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 34	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:  syl5ibcom  245  imbitrrid  246  sbft  2277  dvelimdf  2454  ceqsal1t  3474  gencl  3483  spsbc  3754  ssnelpss  4067  sscon34b  4257  dfnfc2  4886  uniintsn  4941  prex  5383  copsexgw  5439  copsexg  5440  posn  5711  optocl  5719  optoclOLD  5720  funimass1  6575  f1ocnvb  6788  eqfnfv2  6979  elpreima  7005  fconst5  7154  dff13  7202  f1ocnvfv  7226  f1ocnvfvb  7227  fliftfun  7260  eusvobj2  7352  sorpsscmpl  7681  ssonprc  7734  dmfex  7849  xpexr  7862  xpexcnv  7864  relcnvexb  7870  frxp  8070  mpoxopn0yelv  8157  rntpos  8183  oawordeulem  8483  oalimcl  8489  odi  8508  omeulem2  8512  oeeulem  8531  nnasmo  8593  erexb  8663  findcard2  9093  unxpdomlem2  9161  dif1ennnALT  9181  enp1ilem  9182  isfinite2  9202  fodomfib  9233  fodomfibOLD  9235  inf0  9534  rankxplim2  9796  scott0  9802  djuexb  9825  ficardom  9877  cardaleph  10003  dfac5  10043  cflim2  10177  fin23lem23  10240  fin23lem28  10254  isf32lem5  10271  domtriomlem  10356  ac6num  10393  zorn2lem5  10414  zorn2lem6  10415  iunfo  10453  axrepndlem2  10508  axregnd  10519  hargch  10588  addcanpi  10814  mulcanpi  10815  indpi  10822  ltaddnq  10889  ltexnq  10890  prlem934  10948  ltaddpr2  10950  ltaprlem  10959  supsrlem  11026  ssxr  11206  ltxrlt  11207  addcan  11321  addcan2  11322  neg11  11436  negreb  11450  mulcand  11774  receu  11786  ldiv  11979  lemul1a  11999  cju  12145  nn1suc  12171  nnaddcl  12172  nndivtr  12196  znegclb  12532  zmulcl  12544  zeo  12582  uz11  12780  uzp1  12792  eqreznegel  12851  rpnnen1lem6  12899  xrltne  13081  xneg11  13134  xnegdi  13167  xrsupss  13228  xrinfmss  13229  elfznelfzob  13694  modadd1  13832  modmul1  13851  om2uzlti  13877  bccmpl  14236  hashen  14274  fz1eqb  14281  hashfn  14302  hashnn0n0nn  14318  hashtpg  14412  eqwrd  14484  ccatopth  14643  ccatopth2  14644  swrdccatin2  14656  cj11  15089  rennim  15166  cnpart  15167  sqrmo  15178  sqrtgt0  15185  sqreulem  15287  sqreu  15288  cnsqrt00  15320  lo1o1  15459  lo1eq  15495  rlimeq  15496  sumss  15651  cvgcmp  15743  fprodser  15876  efne0d  16024  efne0OLD  16026  dvdsabseq  16244  divalglem8  16331  bitsinv1lem  16372  pcfac  16831  prmreclem3  16850  sectmon  17710  yoniso  18212  oduposb  18254  lublecllem  18285  chnrev  18554  mgmb1mgm1  18584  sgrp2rid2  18855  grpinveu  18908  grpinv11  18941  mulgass  19045  galcan  19237  symg1bas  19324  cayleylem2  19346  odbezout  19491  odeq1  19493  dprddomcld  19936  dvreq1  20351  unitrrg  20640  frgpcyg  21532  obslbs  21689  coe1tm  22219  tgss3  22934  uptx  23573  txindislem  23581  qtopeu  23664  hmeocnvb  23722  qtophmeo  23765  trufil  23858  ufinffr  23877  ghmcnp  24063  tgioo  24744  lmmcvg  25221  bcth3  25291  ovolunlem1a  25457  vitali  25574  ismbf  25589  ismbfcn  25590  rolle  25954  itgsubstlem  26015  vieta1lem2  26279  elqaalem3  26289  aacjcl  26295  efif1olem4  26514  lognegb  26559  logcj  26575  argimgt0  26581  logdmnrp  26610  logcnlem3  26613  logrec  26733  dcubic  26816  isppw  27084  rplogsumlem2  27456  pntpbnd1  27557  sltres  27634  nosupno  27675  nosupres  27679  noinfno  27690  noinfres  27694  negs11  28031  divsmo  28166  n0subs  28342  n0sltp1le  28344  zs12negsclb  28460  axlowdimlem16  29013  usgr0vb  29293  nbgrssvwo2  29418  redwlk  29727  usgr2pthspth  29818  usgr2pth  29820  wlkswwlksf1o  29935  wlklnwwlkln2lem  29938  wpthswwlks2on  30020  clwlkclwwlkf  30066  wwlksubclwwlk  30116  frgr0v  30320  grpoinveu  30577  grpoinvf  30590  diporthcom  30774  norm1exi  31308  shmodsi  31447  shmodi  31448  dfch2  31465  orthin  31504  chssoc  31554  spansncvi  31710  kbpj  32014  lnopunilem1  32068  cnlnssadj  32138  bra11  32166  strlem4  32312  strlem5  32313  hstrlem4  32320  hstrlem5  32321  dmdmd  32358  mdslle1i  32375  mdslle2i  32376  mdslmd1lem1  32383  atcvatlem  32443  atcvat4i  32455  mdsymlem3  32463  bcm1n  32856  xmulcand  32983  xreceu  32984  tpr2rico  34050  bnj1125  35129  revwlkb  35301  umgr2cycllem  35315  mrsubff1  35689  mvhf1  35734  funpsstri  35941  btwnintr  36194  idinside  36259  btwnconn1lem13  36274  fneval  36527  bj-equsal1t  36998  bj-brrelex12ALT  37243  bj-elid6  37346  bj-isrvec2  37476  bj-bary1lem1  37487  bj-bary1  37488  fvineqsnf1  37586  wl-equsal1i  37720  uncf  37771  matunitlindflem2  37789  poimirlem4  37796  poimirlem9  37801  ismtybndlem  37978  grpoeqdivid  38053  0rngo  38199  dmqseqim  38913  eldisjdmqsim2  38988  qmapeldisjsim  39032  rnqmapeleldisjsim  39034  ax12indalem  39242  ax12inda2ALT  39243  lcvexchlem4  39334  lcvexchlem5  39335  opcon3b  39493  2dim  39767  ps-1  39774  paddclN  40139  ltrnnid  40433  cdleme22b  40638  dihmeetlem13N  41616  dih1dimatlem  41626  dihlspsnat  41630  eqresfnbd  42525  remulcan2d  42548  nnaddcom  42559  log11d  42637  sn-addcand  42711  sn-addcan2d  42713  rediveud  42734  onsupneqmaxlim0  43502  sqrtcval  43918  frege58c  44198  gneispa  44407  nzss  44594  expgrowth  44612  sbiota1  44711  ormkglobd  47155  f1cof1b  47359  f1ocof1ob2  47364  fafv2elrnb  47517  sbgoldbwt  48059  dignn0flhalflem1  48897  rrxlinesc  49017  oppff1  49429  aacllem  50082