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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  syl5ibcom  248  imbitrrid  249  sbft  2303  dvelimdf  2478  ceqsal1t  3482  gencl  3491  spsbc  3751  ssnelpss  4062  sscon34b  4249  dfnfc2  4888  uniintsn  4944  prexOLD  5400  copsexgwOLD  5459  copsexg  5460  posn  5733  optocl  5741  optoclOLD  5742  funimass1  6610  f1ocnvb  6826  eqfnfv2  7018  elpreima  7045  fconst5  7200  dff13  7246  f1ocnvfv  7274  f1ocnvfvb  7275  fliftfun  7308  eusvobj2  7400  sorpsscmpl  7733  ssonprc  7784  dmfex  7900  xpexr  7913  xpexcnv  7915  relcnvexb  7921  frxp  8121  mpoxopn0yelv  8208  rntpos  8234  oawordeulem  8540  oalimcl  8546  odi  8565  omeulem2  8569  oeeulem  8588  nnasmo  8650  erexb  8721  uncf  8869  findcard2  9158  unxpdomlem2  9226  dif1ennnALT  9246  enp1ilem  9247  isfinite2  9268  fodomfib  9298  inf0  9600  rankxplim2  9870  scott0b  9909  scott0OLD  9910  djuexb  9962  ficardom  10014  cardaleph  10140  dfac5  10179  cflim2  10313  fin23lem23  10376  fin23lem28  10390  isf32lem5  10407  domtriomlem  10492  ac6num  10529  zorn2lem5  10550  zorn2lem6  10551  iunfo  10595  axrepndlem2  10650  axregnd  10661  hargch  10730  addcanpi  10956  mulcanpi  10957  indpi  10964  ltaddnq  11031  ltexnq  11032  prlem934  11090  ltaddpr2  11092  ltaprlem  11101  supsrlem  11168  ssxr  11351  ltxrlt  11352  addcan  11466  addcan2  11467  neg11  11581  negreb  11595  mulcand  11919  receu  11931  ldiv  12121  lemul1a  12141  cju  12286  nn1suc  12327  nnaddcl  12328  nnaddcom  12332  nndivtr  12355  znegclb  12703  zmulcl  12715  zeo  12755  uz11  12960  uzp1  12972  eqreznegel  13031  rpnnen1lem6  13080  xrltne  13262  xneg11  13315  xnegdi  13348  xrsupss  13409  xrinfmss  13410  elfznelfzob  13878  modadd1  14017  modmul1  14036  om2uzlti  14062  bccmpl  14421  hashen  14459  fz1eqb  14466  hashfn  14487  hashnn0n0nn  14503  hashtpg  14598  eqwrd  14670  ccatopth  14833  ccatopth2  14834  swrdccatin2  14846  cj11  15297  rennim  15374  cnpart  15375  sqrmo  15386  sqrtgt0  15393  sqreulem  15495  sqreu  15496  cnsqrt00  15528  lo1o1  15667  lo1eq  15703  rlimeq  15704  sumss  15858  cvgcmp  15951  fprodser  16084  efne0d  16231  efne0OLD  16233  dvdsabseq  16451  divalglem8  16538  bitsinv1lem  16579  pcfac  17039  prmreclem3  17058  sectmon  17919  yoniso  18421  oduposb  18463  lublecllem  18494  chnrev  18763  mgmb1mgm1  18795  sgrp2rid2  19087  grpinveu  19147  grpinv11  19180  mulgass  19283  galcan  19480  symg1bas  19567  cayleylem2  19589  odbezout  19734  odeq1  19736  dprddomcld  20179  dvreq1  20603  unitrrg  20917  frgpcyg  21841  obslbs  21998  coe1tm  22554  matunitlindflem2  22957  tgss3  23266  uptx  23906  txindislem  23914  qtopeu  23997  hmeocnvb  24055  qtophmeo  24098  trufil  24191  ufinffr  24210  ghmcnp  24396  tgioo  25077  lmmcvg  25544  bcth3  25614  ovolunlem1a  25779  vitali  25896  ismbf  25911  ismbfcn  25912  rolle  26272  itgsubstlem  26330  vieta1lem2  26598  elqaalem3  26608  aacjcl  26618  efif1olem4  26837  lognegb  26882  logcj  26898  argimgt0  26904  logdmnrp  26933  logcnlem3  26936  logrec  27055  dcubic  27138  isppw  27405  rplogsumlem2  27776  pntpbnd1  27877  ltsres  27953  nosupno  27994  nosupres  27998  noinfno  28009  noinfres  28013  negs11  28369  divsmo  28504  n0subs  28683  n0ltsp1le  28685  z12negsclb  28801  axlowdimlem16  29469  usgr0vb  29752  nbgrssvwo2  29877  redwlk  30185  usgr2pthspth  30282  usgr2pth  30284  wlkswwlksf1o  30402  wlklnwwlkln2lem  30405  wpthswwlks2on  30487  clwlkclwwlkf  30533  wwlksubclwwlk  30583  frgr0v  30797  grpoinveu  31055  grpoinvf  31068  diporthcom  31252  norm1exi  31786  shmodsi  31925  shmodi  31926  dfch2  31943  orthin  31982  chssoc  32032  spansncvi  32188  kbpj  32492  lnopunilem1  32546  cnlnssadj  32616  bra11  32644  strlem4  32790  strlem5  32791  hstrlem4  32798  hstrlem5  32799  dmdmd  32836  mdslle1i  32853  mdslle2i  32854  mdslmd1lem1  32861  atcvatlem  32921  atcvat4i  32933  mdsymlem3  32941  bcm1n  33321  xmulcand  33421  xreceu  33422  tpr2rico  34478  bnj1125  35557  fnfvintima  35647  revwlkb  35829  mrsubff1  36200  mvhf1  36245  funpsstri  36452  btwnintr  36706  idinside  36771  btwnconn1lem13  36786  fneval  37062  bj-equsal1t  37656  bj-brrelex12ALT  37902  bj-elid6  38011  bj-isrvec2  38141  bj-bary1lem1  38152  bj-bary1  38153  fvineqsnf1  38253  wl-equsal1i  38396  poimirlem4  38462  poimirlem9  38467  ismtybndlem  38660  grpoeqdivid  38735  0rngo  38881  dmqseqim  39593  eldisjdmqsim2  39668  qmapeldisjsim  39712  rnqmapeleldisjsim  39714  ax12indalem  39922  ax12inda2ALT  39923  lcvexchlem4  40014  lcvexchlem5  40015  opcon3b  40173  2dim  40447  ps-1  40454  paddclN  40819  ltrnnid  41113  cdleme22b  41318  dihmeetlem13N  42296  dih1dimatlem  42306  dihlspsnat  42310  eqresfnbd  43206  remulcan2d  43227  log11d  43325  sn-addcand  43399  sn-addcan2d  43401  rediveud  43422  onsupneqmaxlim0  44169  sqrtcval  44585  frege58c  44865  gneispa  45074  nzss  45245  expgrowth  45263  sbiota1  45362  ormkglobd  47809  f1cof1b  48069  f1ocof1ob2  48074  fafv2elrnb  48227  sbgoldbwt  48797  dignn0flhalflem1  49649  rrxlinesc  49769  oppff1  50178  aacllem  50861