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  2274  dvelimdf  2451  ceqsal1t  3471  gencl  3480  spsbc  3751  ssnelpss  4065  sscon34b  4255  dfnfc2  4882  uniintsn  4937  prex  5379  copsexgw  5435  copsexg  5436  posn  5707  optocl  5715  optoclOLD  5716  funimass1  6571  f1ocnvb  6784  eqfnfv2  6974  elpreima  7000  fconst5  7149  dff13  7197  f1ocnvfv  7221  f1ocnvfvb  7222  fliftfun  7255  eusvobj2  7347  sorpsscmpl  7676  ssonprc  7729  dmfex  7844  xpexr  7857  xpexcnv  7859  relcnvexb  7865  frxp  8065  mpoxopn0yelv  8152  rntpos  8178  oawordeulem  8478  oalimcl  8484  odi  8503  omeulem2  8507  oeeulem  8525  nnasmo  8587  erexb  8656  findcard2  9084  unxpdomlem2  9151  dif1ennnALT  9171  enp1ilem  9172  isfinite2  9192  fodomfib  9223  fodomfibOLD  9225  inf0  9521  rankxplim2  9783  scott0  9789  djuexb  9812  ficardom  9864  cardaleph  9990  dfac5  10030  cflim2  10164  fin23lem23  10227  fin23lem28  10241  isf32lem5  10258  domtriomlem  10343  ac6num  10380  zorn2lem5  10401  zorn2lem6  10402  iunfo  10440  axrepndlem2  10494  axregnd  10505  hargch  10574  addcanpi  10800  mulcanpi  10801  indpi  10808  ltaddnq  10875  ltexnq  10876  prlem934  10934  ltaddpr2  10936  ltaprlem  10945  supsrlem  11012  ssxr  11192  ltxrlt  11193  addcan  11307  addcan2  11308  neg11  11422  negreb  11436  mulcand  11760  receu  11772  ldiv  11965  lemul1a  11985  cju  12131  nn1suc  12157  nnaddcl  12158  nndivtr  12182  znegclb  12519  zmulcl  12531  zeo  12569  uz11  12767  uzp1  12783  eqreznegel  12842  rpnnen1lem6  12890  xrltne  13072  xneg11  13124  xnegdi  13157  xrsupss  13218  xrinfmss  13219  elfznelfzob  13684  modadd1  13822  modmul1  13841  om2uzlti  13867  bccmpl  14226  hashen  14264  fz1eqb  14271  hashfn  14292  hashnn0n0nn  14308  hashtpg  14402  eqwrd  14474  ccatopth  14633  ccatopth2  14634  swrdccatin2  14646  cj11  15079  rennim  15156  cnpart  15157  sqrmo  15168  sqrtgt0  15175  sqreulem  15277  sqreu  15278  cnsqrt00  15310  lo1o1  15449  lo1eq  15485  rlimeq  15486  sumss  15641  cvgcmp  15733  fprodser  15866  efne0d  16014  efne0OLD  16016  dvdsabseq  16234  divalglem8  16321  bitsinv1lem  16362  pcfac  16821  prmreclem3  16840  sectmon  17699  yoniso  18201  oduposb  18243  lublecllem  18274  chnrev  18543  mgmb1mgm1  18573  sgrp2rid2  18844  grpinveu  18897  grpinv11  18930  mulgass  19034  galcan  19226  symg1bas  19313  cayleylem2  19335  odbezout  19480  odeq1  19482  dprddomcld  19925  dvreq1  20339  unitrrg  20628  frgpcyg  21520  obslbs  21677  coe1tm  22197  tgss3  22911  uptx  23550  txindislem  23558  qtopeu  23641  hmeocnvb  23699  qtophmeo  23742  trufil  23835  ufinffr  23854  ghmcnp  24040  tgioo  24721  lmmcvg  25198  bcth3  25268  ovolunlem1a  25434  vitali  25551  ismbf  25566  ismbfcn  25567  rolle  25931  itgsubstlem  25992  vieta1lem2  26256  elqaalem3  26266  aacjcl  26272  efif1olem4  26491  lognegb  26536  logcj  26552  argimgt0  26558  logdmnrp  26587  logcnlem3  26590  logrec  26710  dcubic  26793  isppw  27061  rplogsumlem2  27433  pntpbnd1  27534  sltres  27611  nosupno  27652  nosupres  27656  noinfno  27667  noinfres  27671  negs11  28001  divsmo  28133  n0subs  28299  n0sltp1le  28301  zs12negsclb  28401  axlowdimlem16  28946  usgr0vb  29226  nbgrssvwo2  29351  redwlk  29660  usgr2pthspth  29751  usgr2pth  29753  wlkswwlksf1o  29868  wlklnwwlkln2lem  29871  wpthswwlks2on  29953  clwlkclwwlkf  29999  wwlksubclwwlk  30049  frgr0v  30253  grpoinveu  30510  grpoinvf  30523  diporthcom  30707  norm1exi  31241  shmodsi  31380  shmodi  31381  dfch2  31398  orthin  31437  chssoc  31487  spansncvi  31643  kbpj  31947  lnopunilem1  32001  cnlnssadj  32071  bra11  32099  strlem4  32245  strlem5  32246  hstrlem4  32253  hstrlem5  32254  dmdmd  32291  mdslle1i  32308  mdslle2i  32309  mdslmd1lem1  32316  atcvatlem  32376  atcvat4i  32388  mdsymlem3  32396  bcm1n  32788  xmulcand  32912  xreceu  32913  tpr2rico  33936  bnj1125  35015  revwlkb  35181  umgr2cycllem  35195  mrsubff1  35569  mvhf1  35614  funpsstri  35821  btwnintr  36074  idinside  36139  btwnconn1lem13  36154  fneval  36407  bj-equsal1t  36877  bj-brrelex12ALT  37122  bj-elid6  37225  bj-isrvec2  37355  bj-bary1lem1  37366  bj-bary1  37367  fvineqsnf1  37465  wl-equsal1i  37599  uncf  37649  matunitlindflem2  37667  poimirlem4  37674  poimirlem9  37679  ismtybndlem  37856  grpoeqdivid  37931  0rngo  38077  dmqseqim  38764  ax12indalem  39054  ax12inda2ALT  39055  lcvexchlem4  39146  lcvexchlem5  39147  opcon3b  39305  2dim  39579  ps-1  39586  paddclN  39951  ltrnnid  40245  cdleme22b  40450  dihmeetlem13N  41428  dih1dimatlem  41438  dihlspsnat  41442  eqresfnbd  42340  remulcan2d  42365  nnaddcom  42376  log11d  42454  sn-addcand  42528  sn-addcan2d  42530  rediveud  42551  onsupneqmaxlim0  43331  sqrtcval  43748  frege58c  44028  gneispa  44237  nzss  44424  expgrowth  44442  sbiota1  44541  ormkglobd  46987  f1cof1b  47191  f1ocof1ob2  47196  fafv2elrnb  47349  sbgoldbwt  47891  dignn0flhalflem1  48730  rrxlinesc  48850  oppff1  49263  aacllem  49916