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  2271  dvelimdf  2448  ceqsal1t  3467  gencl  3476  spsbc  3752  ssnelpss  4062  sscon34b  4252  dfnfc2  4879  uniintsn  4933  prex  5373  copsexgw  5428  copsexg  5429  posn  5700  optocl  5708  optoclOLD  5709  funimass1  6559  f1ocnvb  6772  eqfnfv2  6960  elpreima  6986  fconst5  7135  dff13  7183  f1ocnvfv  7207  f1ocnvfvb  7208  fliftfun  7241  eusvobj2  7333  sorpsscmpl  7662  ssonprc  7715  dmfex  7830  xpexr  7843  xpexcnv  7845  relcnvexb  7851  frxp  8051  mpoxopn0yelv  8138  rntpos  8164  oawordeulem  8464  oalimcl  8470  odi  8489  omeulem2  8493  oeeulem  8511  nnasmo  8573  erexb  8642  findcard2  9069  unxpdomlem2  9136  dif1ennnALT  9156  enp1ilem  9157  isfinite2  9177  fodomfib  9208  fodomfibOLD  9210  inf0  9506  rankxplim2  9765  scott0  9771  djuexb  9794  ficardom  9846  cardaleph  9972  dfac5  10012  cflim2  10146  fin23lem23  10209  fin23lem28  10223  isf32lem5  10240  domtriomlem  10325  ac6num  10362  zorn2lem5  10383  zorn2lem6  10384  iunfo  10422  axrepndlem2  10476  axregnd  10487  hargch  10556  addcanpi  10782  mulcanpi  10783  indpi  10790  ltaddnq  10857  ltexnq  10858  prlem934  10916  ltaddpr2  10918  ltaprlem  10927  supsrlem  10994  ssxr  11174  ltxrlt  11175  addcan  11289  addcan2  11290  neg11  11404  negreb  11418  mulcand  11742  receu  11754  ldiv  11947  lemul1a  11967  cju  12113  nn1suc  12139  nnaddcl  12140  nndivtr  12164  znegclb  12501  zmulcl  12513  zeo  12551  uz11  12749  uzp1  12765  eqreznegel  12824  rpnnen1lem6  12872  xrltne  13054  xneg11  13106  xnegdi  13139  xrsupss  13200  xrinfmss  13201  elfznelfzob  13666  modadd1  13804  modmul1  13823  om2uzlti  13849  bccmpl  14208  hashen  14246  fz1eqb  14253  hashfn  14274  hashnn0n0nn  14290  hashtpg  14384  eqwrd  14456  ccatopth  14615  ccatopth2  14616  swrdccatin2  14628  cj11  15061  rennim  15138  cnpart  15139  sqrmo  15150  sqrtgt0  15157  sqreulem  15259  sqreu  15260  cnsqrt00  15292  lo1o1  15431  lo1eq  15467  rlimeq  15468  sumss  15623  cvgcmp  15715  fprodser  15848  efne0d  15996  efne0OLD  15998  dvdsabseq  16216  divalglem8  16303  bitsinv1lem  16344  pcfac  16803  prmreclem3  16822  sectmon  17681  yoniso  18183  oduposb  18225  lublecllem  18256  chnrev  18525  mgmb1mgm1  18555  sgrp2rid2  18826  grpinveu  18879  grpinv11  18912  mulgass  19016  galcan  19209  symg1bas  19296  cayleylem2  19318  odbezout  19463  odeq1  19465  dprddomcld  19908  dvreq1  20322  unitrrg  20611  frgpcyg  21503  obslbs  21660  coe1tm  22180  tgss3  22894  uptx  23533  txindislem  23541  qtopeu  23624  hmeocnvb  23682  qtophmeo  23725  trufil  23818  ufinffr  23837  ghmcnp  24023  tgioo  24704  lmmcvg  25181  bcth3  25251  ovolunlem1a  25417  vitali  25534  ismbf  25549  ismbfcn  25550  rolle  25914  itgsubstlem  25975  vieta1lem2  26239  elqaalem3  26249  aacjcl  26255  efif1olem4  26474  lognegb  26519  logcj  26535  argimgt0  26541  logdmnrp  26570  logcnlem3  26573  logrec  26693  dcubic  26776  isppw  27044  rplogsumlem2  27416  pntpbnd1  27517  sltres  27594  nosupno  27635  nosupres  27639  noinfno  27650  noinfres  27654  negs11  27984  divsmo  28116  n0subs  28282  n0sltp1le  28284  zs12negsclb  28384  axlowdimlem16  28928  usgr0vb  29208  nbgrssvwo2  29333  redwlk  29642  usgr2pthspth  29733  usgr2pth  29735  wlkswwlksf1o  29850  wlklnwwlkln2lem  29853  wpthswwlks2on  29932  clwlkclwwlkf  29978  wwlksubclwwlk  30028  frgr0v  30232  grpoinveu  30489  grpoinvf  30502  diporthcom  30686  norm1exi  31220  shmodsi  31359  shmodi  31360  dfch2  31377  orthin  31416  chssoc  31466  spansncvi  31622  kbpj  31926  lnopunilem1  31980  cnlnssadj  32050  bra11  32078  strlem4  32224  strlem5  32225  hstrlem4  32232  hstrlem5  32233  dmdmd  32270  mdslle1i  32287  mdslle2i  32288  mdslmd1lem1  32295  atcvatlem  32355  atcvat4i  32367  mdsymlem3  32375  bcm1n  32767  xmulcand  32891  xreceu  32892  tpr2rico  33915  bnj1125  34994  revwlkb  35138  umgr2cycllem  35152  mrsubff1  35526  mvhf1  35571  funpsstri  35778  btwnintr  36032  idinside  36097  btwnconn1lem13  36112  fneval  36365  bj-equsal1t  36835  bj-brrelex12ALT  37080  bj-elid6  37183  bj-isrvec2  37313  bj-bary1lem1  37324  bj-bary1  37325  fvineqsnf1  37423  wl-equsal1i  37557  uncf  37618  matunitlindflem2  37636  poimirlem4  37643  poimirlem9  37648  ismtybndlem  37825  grpoeqdivid  37900  0rngo  38046  dmqseqim  38673  ax12indalem  38963  ax12inda2ALT  38964  lcvexchlem4  39055  lcvexchlem5  39056  opcon3b  39214  2dim  39488  ps-1  39495  paddclN  39860  ltrnnid  40154  cdleme22b  40359  dihmeetlem13N  41337  dih1dimatlem  41347  dihlspsnat  41351  eqresfnbd  42244  remulcan2d  42269  nnaddcom  42280  log11d  42358  sn-addcand  42432  sn-addcan2d  42434  rediveud  42455  onsupneqmaxlim0  43236  sqrtcval  43653  frege58c  43933  gneispa  44142  nzss  44329  expgrowth  44347  sbiota1  44446  ormkglobd  46892  f1cof1b  47087  f1ocof1ob2  47092  fafv2elrnb  47245  sbgoldbwt  47787  dignn0flhalflem1  48626  rrxlinesc  48746  oppff1  49159  aacllem  49812