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  2270  dvelimdf  2454  ceqsal1t  3514  gencl  3523  spsbc  3801  ssnelpss  4114  sscon34b  4304  dfnfc2  4929  uniintsn  4985  prex  5437  copsexgw  5495  copsexg  5496  posn  5771  optocl  5780  funimass1  6648  f1ocnvb  6861  eqfnfv2  7052  elpreima  7078  fconst5  7226  dff13  7275  f1ocnvfv  7298  f1ocnvfvb  7299  fliftfun  7332  eusvobj2  7423  sorpsscmpl  7754  ssonprc  7807  dmfex  7927  xpexr  7940  xpexcnv  7942  relcnvexb  7948  frxp  8151  mpoxopn0yelv  8238  rntpos  8264  oawordeulem  8592  oalimcl  8598  odi  8617  omeulem2  8621  oeeulem  8639  nnasmo  8701  erexb  8770  findcard2  9204  unxpdomlem2  9287  dif1ennnALT  9311  enp1ilem  9312  isfinite2  9334  fodomfib  9369  fodomfibOLD  9371  inf0  9661  rankxplim2  9920  scott0  9926  djuexb  9949  ficardom  10001  cardaleph  10129  dfac5  10169  cflim2  10303  fin23lem23  10366  fin23lem28  10380  isf32lem5  10397  domtriomlem  10482  ac6num  10519  zorn2lem5  10540  zorn2lem6  10541  iunfo  10579  axrepndlem2  10633  axregnd  10644  hargch  10713  addcanpi  10939  mulcanpi  10940  indpi  10947  ltaddnq  11014  ltexnq  11015  prlem934  11073  ltaddpr2  11075  ltaprlem  11084  supsrlem  11151  ssxr  11330  ltxrlt  11331  addcan  11445  addcan2  11446  neg11  11560  negreb  11574  mulcand  11896  receu  11908  ldiv  12101  lemul1a  12121  cju  12262  nn1suc  12288  nnaddcl  12289  nndivtr  12313  znegclb  12654  zmulcl  12666  zeo  12704  uz11  12903  uzp1  12919  eqreznegel  12976  rpnnen1lem6  13024  xrltne  13205  xneg11  13257  xnegdi  13290  xrsupss  13351  xrinfmss  13352  elfznelfzob  13812  modadd1  13948  modmul1  13965  om2uzlti  13991  bccmpl  14348  hashen  14386  fz1eqb  14393  hashfn  14414  hashnn0n0nn  14430  hashtpg  14524  eqwrd  14595  ccatopth  14754  ccatopth2  14755  swrdccatin2  14767  cj11  15201  rennim  15278  cnpart  15279  sqrmo  15290  sqrtgt0  15297  sqreulem  15398  sqreu  15399  cnsqrt00  15431  lo1o1  15568  lo1eq  15604  rlimeq  15605  sumss  15760  cvgcmp  15852  fprodser  15985  efne0  16133  dvdsabseq  16350  divalglem8  16437  bitsinv1lem  16478  pcfac  16937  prmreclem3  16956  sectmon  17826  yoniso  18330  oduposb  18374  lublecllem  18405  mgmb1mgm1  18668  sgrp2rid2  18939  grpinveu  18992  grpinv11  19025  mulgass  19129  galcan  19322  symg1bas  19408  cayleylem2  19431  odbezout  19576  odeq1  19578  dprddomcld  20021  dvreq1  20411  unitrrg  20703  frgpcyg  21592  obslbs  21750  coe1tm  22276  tgss3  22993  uptx  23633  txindislem  23641  qtopeu  23724  hmeocnvb  23782  qtophmeo  23825  trufil  23918  ufinffr  23937  ghmcnp  24123  tgioo  24817  lmmcvg  25295  bcth3  25365  ovolunlem1a  25531  vitali  25648  ismbf  25663  ismbfcn  25664  rolle  26028  itgsubstlem  26089  vieta1lem2  26353  elqaalem3  26363  aacjcl  26369  efif1olem4  26587  lognegb  26632  logcj  26648  argimgt0  26654  logdmnrp  26683  logcnlem3  26686  logrec  26806  dcubic  26889  isppw  27157  rplogsumlem2  27529  pntpbnd1  27630  sltres  27707  nosupno  27748  nosupres  27752  noinfno  27763  noinfres  27767  negs11  28081  divsmo  28210  n0subs  28360  axlowdimlem16  28972  usgr0vb  29254  nbgrssvwo2  29379  redwlk  29690  usgr2pthspth  29782  usgr2pth  29784  wlkswwlksf1o  29899  wlklnwwlkln2lem  29902  wpthswwlks2on  29981  clwlkclwwlkf  30027  wwlksubclwwlk  30077  frgr0v  30281  grpoinveu  30538  grpoinvf  30551  diporthcom  30735  norm1exi  31269  shmodsi  31408  shmodi  31409  dfch2  31426  orthin  31465  chssoc  31515  spansncvi  31671  kbpj  31975  lnopunilem1  32029  cnlnssadj  32099  bra11  32127  strlem4  32273  strlem5  32274  hstrlem4  32281  hstrlem5  32282  dmdmd  32319  mdslle1i  32336  mdslle2i  32337  mdslmd1lem1  32344  atcvatlem  32404  atcvat4i  32416  mdsymlem3  32424  bcm1n  32797  xmulcand  32903  xreceu  32904  tpr2rico  33911  bnj1125  35006  revwlkb  35131  umgr2cycllem  35145  mrsubff1  35519  mvhf1  35564  funpsstri  35766  btwnintr  36020  idinside  36085  btwnconn1lem13  36100  fneval  36353  bj-equsal1t  36823  bj-brrelex12ALT  37068  bj-elid6  37171  bj-isrvec2  37301  bj-bary1lem1  37312  bj-bary1  37313  fvineqsnf1  37411  wl-equsal1i  37545  uncf  37606  matunitlindflem2  37624  poimirlem4  37631  poimirlem9  37636  ismtybndlem  37813  grpoeqdivid  37888  0rngo  38034  imaexALTV  38331  dmqseqim  38657  ax12indalem  38946  ax12inda2ALT  38947  lcvexchlem4  39038  lcvexchlem5  39039  opcon3b  39197  2dim  39472  ps-1  39479  paddclN  39844  ltrnnid  40138  cdleme22b  40343  dihmeetlem13N  41321  dih1dimatlem  41331  dihlspsnat  41335  eqresfnbd  42273  remulcan2d  42298  nnaddcom  42303  efne0d  42373  log11d  42382  sn-addcand  42449  sn-addcan2d  42451  onsupneqmaxlim0  43236  sqrtcval  43654  frege58c  43934  gneispa  44143  nzss  44336  expgrowth  44354  sbiota1  44453  ormkglobd  46890  f1cof1b  47089  f1ocof1ob2  47094  fafv2elrnb  47247  sbgoldbwt  47764  dignn0flhalflem1  48536  rrxlinesc  48656  aacllem  49320