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  2448  ceqsal1t  3483  gencl  3492  spsbc  3769  ssnelpss  4080  sscon34b  4270  dfnfc2  4896  uniintsn  4952  prex  5395  copsexgw  5453  copsexg  5454  posn  5727  optocl  5736  funimass1  6601  f1ocnvb  6816  eqfnfv2  7007  elpreima  7033  fconst5  7183  dff13  7232  f1ocnvfv  7256  f1ocnvfvb  7257  fliftfun  7290  eusvobj2  7382  sorpsscmpl  7713  ssonprc  7766  dmfex  7884  xpexr  7897  xpexcnv  7899  relcnvexb  7905  frxp  8108  mpoxopn0yelv  8195  rntpos  8221  oawordeulem  8521  oalimcl  8527  odi  8546  omeulem2  8550  oeeulem  8568  nnasmo  8630  erexb  8699  findcard2  9134  unxpdomlem2  9205  dif1ennnALT  9229  enp1ilem  9230  isfinite2  9252  fodomfib  9287  fodomfibOLD  9289  inf0  9581  rankxplim2  9840  scott0  9846  djuexb  9869  ficardom  9921  cardaleph  10049  dfac5  10089  cflim2  10223  fin23lem23  10286  fin23lem28  10300  isf32lem5  10317  domtriomlem  10402  ac6num  10439  zorn2lem5  10460  zorn2lem6  10461  iunfo  10499  axrepndlem2  10553  axregnd  10564  hargch  10633  addcanpi  10859  mulcanpi  10860  indpi  10867  ltaddnq  10934  ltexnq  10935  prlem934  10993  ltaddpr2  10995  ltaprlem  11004  supsrlem  11071  ssxr  11250  ltxrlt  11251  addcan  11365  addcan2  11366  neg11  11480  negreb  11494  mulcand  11818  receu  11830  ldiv  12023  lemul1a  12043  cju  12189  nn1suc  12215  nnaddcl  12216  nndivtr  12240  znegclb  12577  zmulcl  12589  zeo  12627  uz11  12825  uzp1  12841  eqreznegel  12900  rpnnen1lem6  12948  xrltne  13130  xneg11  13182  xnegdi  13215  xrsupss  13276  xrinfmss  13277  elfznelfzob  13741  modadd1  13877  modmul1  13896  om2uzlti  13922  bccmpl  14281  hashen  14319  fz1eqb  14326  hashfn  14347  hashnn0n0nn  14363  hashtpg  14457  eqwrd  14529  ccatopth  14688  ccatopth2  14689  swrdccatin2  14701  cj11  15135  rennim  15212  cnpart  15213  sqrmo  15224  sqrtgt0  15231  sqreulem  15333  sqreu  15334  cnsqrt00  15366  lo1o1  15505  lo1eq  15541  rlimeq  15542  sumss  15697  cvgcmp  15789  fprodser  15922  efne0d  16070  efne0OLD  16072  dvdsabseq  16290  divalglem8  16377  bitsinv1lem  16418  pcfac  16877  prmreclem3  16896  sectmon  17751  yoniso  18253  oduposb  18295  lublecllem  18326  mgmb1mgm1  18589  sgrp2rid2  18860  grpinveu  18913  grpinv11  18946  mulgass  19050  galcan  19243  symg1bas  19328  cayleylem2  19350  odbezout  19495  odeq1  19497  dprddomcld  19940  dvreq1  20327  unitrrg  20619  frgpcyg  21490  obslbs  21646  coe1tm  22166  tgss3  22880  uptx  23519  txindislem  23527  qtopeu  23610  hmeocnvb  23668  qtophmeo  23711  trufil  23804  ufinffr  23823  ghmcnp  24009  tgioo  24691  lmmcvg  25168  bcth3  25238  ovolunlem1a  25404  vitali  25521  ismbf  25536  ismbfcn  25537  rolle  25901  itgsubstlem  25962  vieta1lem2  26226  elqaalem3  26236  aacjcl  26242  efif1olem4  26461  lognegb  26506  logcj  26522  argimgt0  26528  logdmnrp  26557  logcnlem3  26560  logrec  26680  dcubic  26763  isppw  27031  rplogsumlem2  27403  pntpbnd1  27504  sltres  27581  nosupno  27622  nosupres  27626  noinfno  27637  noinfres  27641  negs11  27962  divsmo  28094  n0subs  28260  n0sltp1le  28262  zs12negsclb  28348  axlowdimlem16  28891  usgr0vb  29171  nbgrssvwo2  29296  redwlk  29607  usgr2pthspth  29699  usgr2pth  29701  wlkswwlksf1o  29816  wlklnwwlkln2lem  29819  wpthswwlks2on  29898  clwlkclwwlkf  29944  wwlksubclwwlk  29994  frgr0v  30198  grpoinveu  30455  grpoinvf  30468  diporthcom  30652  norm1exi  31186  shmodsi  31325  shmodi  31326  dfch2  31343  orthin  31382  chssoc  31432  spansncvi  31588  kbpj  31892  lnopunilem1  31946  cnlnssadj  32016  bra11  32044  strlem4  32190  strlem5  32191  hstrlem4  32198  hstrlem5  32199  dmdmd  32236  mdslle1i  32253  mdslle2i  32254  mdslmd1lem1  32261  atcvatlem  32321  atcvat4i  32333  mdsymlem3  32341  bcm1n  32725  xmulcand  32848  xreceu  32849  tpr2rico  33909  bnj1125  34989  revwlkb  35120  umgr2cycllem  35134  mrsubff1  35508  mvhf1  35553  funpsstri  35760  btwnintr  36014  idinside  36079  btwnconn1lem13  36094  fneval  36347  bj-equsal1t  36817  bj-brrelex12ALT  37062  bj-elid6  37165  bj-isrvec2  37295  bj-bary1lem1  37306  bj-bary1  37307  fvineqsnf1  37405  wl-equsal1i  37539  uncf  37600  matunitlindflem2  37618  poimirlem4  37625  poimirlem9  37630  ismtybndlem  37807  grpoeqdivid  37882  0rngo  38028  dmqseqim  38655  ax12indalem  38945  ax12inda2ALT  38946  lcvexchlem4  39037  lcvexchlem5  39038  opcon3b  39196  2dim  39471  ps-1  39478  paddclN  39843  ltrnnid  40137  cdleme22b  40342  dihmeetlem13N  41320  dih1dimatlem  41330  dihlspsnat  41334  eqresfnbd  42227  remulcan2d  42252  nnaddcom  42263  log11d  42341  sn-addcand  42415  sn-addcan2d  42417  rediveud  42438  onsupneqmaxlim0  43220  sqrtcval  43637  frege58c  43917  gneispa  44126  nzss  44313  expgrowth  44331  sbiota1  44430  ormkglobd  46880  f1cof1b  47082  f1ocof1ob2  47087  fafv2elrnb  47240  sbgoldbwt  47782  dignn0flhalflem1  48608  rrxlinesc  48728  oppff1  49141  aacllem  49794