Theorem imbitrid 247

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 232	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 35	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibcom  248  imbitrrid  249  sbft  2303  dvelimdf  2479  ceqsal1t  3485  gencl  3494  spsbc  3756  ssnelpss  4068  sscon34b  4256  dfnfc2  4893  uniintsn  4949  prexOLD  5414  copsexgwOLD  5473  copsexg  5474  posn  5747  optocl  5755  optoclOLD  5756  funimass1  6618  f1ocnvb  6834  eqfnfv2  7026  elpreima  7053  fconst5  7204  dff13  7252  f1ocnvfv  7276  f1ocnvfvb  7277  fliftfun  7310  eusvobj2  7402  sorpsscmpl  7731  ssonprc  7785  dmfex  7901  xpexr  7914  xpexcnv  7916  relcnvexb  7922  frxp  8121  mpoxopn0yelv  8208  rntpos  8234  oawordeulem  8538  oalimcl  8544  odi  8563  omeulem2  8567  oeeulem  8586  nnasmo  8648  erexb  8719  findcard2  9148  unxpdomlem2  9216  dif1ennnALT  9236  enp1ilem  9237  isfinite2  9257  fodomfib  9287  inf0  9589  rankxplim2  9851  scott0  9859  djuexb  9894  ficardom  9946  cardaleph  10072  dfac5  10111  cflim2  10246  fin23lem23  10309  fin23lem28  10323  isf32lem5  10340  domtriomlem  10425  ac6num  10462  zorn2lem5  10483  zorn2lem6  10484  iunfo  10522  axrepndlem2  10577  axregnd  10588  hargch  10657  addcanpi  10883  mulcanpi  10884  indpi  10891  ltaddnq  10958  ltexnq  10959  prlem934  11017  ltaddpr2  11019  ltaprlem  11028  supsrlem  11095  ssxr  11278  ltxrlt  11279  addcan  11393  addcan2  11394  neg11  11508  negreb  11522  mulcand  11846  receu  11858  ldiv  12048  lemul1a  12068  cju  12213  nn1suc  12254  nnaddcl  12255  nnaddcom  12259  nndivtr  12282  znegclb  12630  zmulcl  12642  zeo  12681  uz11  12886  uzp1  12898  eqreznegel  12957  rpnnen1lem6  13005  xrltne  13187  xneg11  13240  xnegdi  13273  xrsupss  13334  xrinfmss  13335  elfznelfzob  13803  modadd1  13941  modmul1  13960  om2uzlti  13986  bccmpl  14345  hashen  14383  fz1eqb  14390  hashfn  14411  hashnn0n0nn  14427  hashtpg  14522  eqwrd  14594  ccatopth  14753  ccatopth2  14754  swrdccatin2  14766  cj11  15213  rennim  15290  cnpart  15291  sqrmo  15302  sqrtgt0  15309  sqreulem  15411  sqreu  15412  cnsqrt00  15444  lo1o1  15583  lo1eq  15619  rlimeq  15620  sumss  15775  cvgcmp  15868  fprodser  16003  efne0d  16150  efne0OLD  16152  dvdsabseq  16370  divalglem8  16457  bitsinv1lem  16498  pcfac  16958  prmreclem3  16977  sectmon  17838  yoniso  18340  oduposb  18382  lublecllem  18413  chnrev  18682  mgmb1mgm1  18712  sgrp2rid2  18987  grpinveu  19040  grpinv11  19073  mulgass  19176  galcan  19373  symg1bas  19460  cayleylem2  19482  odbezout  19627  odeq1  19629  dprddomcld  20072  dvreq1  20492  unitrrg  20787  frgpcyg  21702  obslbs  21859  coe1tm  22413  tgss3  23122  uptx  23761  txindislem  23769  qtopeu  23852  hmeocnvb  23910  qtophmeo  23953  trufil  24046  ufinffr  24065  ghmcnp  24251  tgioo  24932  lmmcvg  25399  bcth3  25469  ovolunlem1a  25634  vitali  25751  ismbf  25766  ismbfcn  25767  rolle  26128  itgsubstlem  26186  vieta1lem2  26451  elqaalem3  26461  aacjcl  26467  efif1olem4  26686  lognegb  26731  logcj  26747  argimgt0  26753  logdmnrp  26782  logcnlem3  26785  logrec  26904  dcubic  26987  isppw  27254  rplogsumlem2  27625  pntpbnd1  27726  ltsres  27802  nosupno  27843  nosupres  27847  noinfno  27858  noinfres  27862  negs11  28218  divsmo  28353  n0subs  28532  n0ltsp1le  28534  z12negsclb  28650  axlowdimlem16  29273  usgr0vb  29553  nbgrssvwo2  29678  redwlk  29986  usgr2pthspth  30077  usgr2pth  30079  wlkswwlksf1o  30194  wlklnwwlkln2lem  30197  wpthswwlks2on  30279  clwlkclwwlkf  30325  wwlksubclwwlk  30375  frgr0v  30579  grpoinveu  30837  grpoinvf  30850  diporthcom  31034  norm1exi  31568  shmodsi  31707  shmodi  31708  dfch2  31725  orthin  31764  chssoc  31814  spansncvi  31970  kbpj  32274  lnopunilem1  32328  cnlnssadj  32398  bra11  32426  strlem4  32572  strlem5  32573  hstrlem4  32580  hstrlem5  32581  dmdmd  32618  mdslle1i  32635  mdslle2i  32636  mdslmd1lem1  32643  atcvatlem  32703  atcvat4i  32715  mdsymlem3  32723  bcm1n  33106  xmulcand  33206  xreceu  33207  tpr2rico  34268  bnj1125  35346  fnfvintima  35442  revwlkb  35584  umgr2cycllem  35598  mrsubff1  35972  mvhf1  36017  funpsstri  36224  btwnintr  36477  idinside  36542  btwnconn1lem13  36557  fneval  36829  bj-equsal1t  37423  bj-brrelex12ALT  37669  bj-elid6  37780  bj-isrvec2  37910  bj-bary1lem1  37921  bj-bary1  37922  fvineqsnf1  38022  wl-equsal1i  38165  uncf  38216  matunitlindflem2  38234  poimirlem4  38241  poimirlem9  38246  ismtybndlem  38423  grpoeqdivid  38498  0rngo  38644  dmqseqim  39358  eldisjdmqsim2  39433  qmapeldisjsim  39477  rnqmapeleldisjsim  39479  ax12indalem  39687  ax12inda2ALT  39688  lcvexchlem4  39779  lcvexchlem5  39780  opcon3b  39938  2dim  40212  ps-1  40219  paddclN  40584  ltrnnid  40878  cdleme22b  41083  dihmeetlem13N  42061  dih1dimatlem  42071  dihlspsnat  42075  eqresfnbd  42971  remulcan2d  42992  log11d  43075  sn-addcand  43149  sn-addcan2d  43151  rediveud  43172  onsupneqmaxlim0  43921  sqrtcval  44337  frege58c  44617  gneispa  44826  nzss  44997  expgrowth  45015  sbiota1  45114  ormkglobd  47561  f1cof1b  47781  f1ocof1ob2  47786  fafv2elrnb  47939  sbgoldbwt  48509  dignn0flhalflem1  49362  rrxlinesc  49482  oppff1  49893  aacllem  50568