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  2307  dvelimdf  2481  ceqsal1t  3486  gencl  3495  spsbc  3755  ssnelpss  4045  sscon34b  4252  dfnfc2  4892  uniintsn  4948  prexOLD  5405  copsexgwOLD  5465  copsexg  5466  posn  5742  optocl  5750  optoclOLD  5751  funimass1  6644  f1ocnvb  6860  eqfnfv2  7053  elpreima  7080  elpreimaOLD  7081  fconst5  7235  dff13  7281  f1ocnvfv  7309  f1ocnvfvb  7310  fliftfun  7343  eusvobj2  7435  sorpsscmpl  7774  ssonprc  7825  dmfex  7941  xpexr  7954  xpexcnv  7956  relcnvexb  7962  frxp  8165  mpoxopn0yelv  8258  rntpos  8284  oawordeulem  8590  oalimcl  8596  odi  8615  omeulem2  8619  oeeulem  8638  nnasmo  8700  erexb  8771  uncf  8919  findcard2  9208  unxpdomlem2  9276  dif1ennnALT  9296  enp1ilem  9297  isfinite2  9318  fodomfib  9348  inf0  9649  rankxplim2  9924  scott0b  9964  scott0OLD  9965  djuexb  10017  ficardom  10069  cardaleph  10195  dfac5  10234  cflim2  10368  fin23lem23  10431  fin23lem28  10445  isf32lem5  10462  domtriomlem  10547  ac6num  10584  zorn2lem5  10605  zorn2lem6  10606  iunfo  10650  axrepndlem2  10705  axregnd  10716  hargch  10785  addcanpi  11011  mulcanpi  11012  indpi  11019  ltaddnq  11086  ltexnq  11087  prlem934  11145  ltaddpr2  11147  ltaprlem  11156  supsrlem  11223  ssxr  11406  ltxrlt  11407  addcan  11521  addcan2  11522  neg11  11636  negreb  11650  mulcand  11976  receu  11988  ldiv  12178  lemul1a  12198  cju  12343  nn1suc  12384  nnaddcl  12385  nnaddcom  12389  nndivtr  12412  znegclb  12760  zmulcl  12772  zeo  12812  uz11  13017  uzp1  13029  eqreznegel  13088  rpnnen1lem6  13137  xrltne  13319  xneg11  13372  xnegdi  13405  xrsupss  13466  xrinfmss  13467  elfznelfzob  13936  modadd1  14075  modmul1  14094  om2uzlti  14120  bccmpl  14480  hashen  14518  fz1eqb  14525  hashfn  14546  hashnn0n0nn  14562  hashtpg  14657  eqwrd  14729  ccatopth  14893  ccatopth2  14894  swrdccatin2  14906  cj11  15358  rennim  15435  cnpart  15436  sqrmo  15447  sqrtgt0  15454  sqreulem  15556  sqreu  15557  cnsqrt00  15589  lo1o1  15728  lo1eq  15764  rlimeq  15765  sumss  15919  cvgcmp  16012  fprodser  16145  efne0d  16292  efne0OLD  16294  dvdsabseq  16512  divalglem8  16599  bitsinv1lem  16640  pcfac  17106  prmreclem3  17125  sectmon  17986  yoniso  18488  oduposb  18530  lublecllem  18561  chnrev  18830  mgmb1mgm1  18862  sgrp2rid2  19154  grpinveu  19214  grpinv11  19247  mulgass  19350  galcan  19548  symg1bas  19635  cayleylem2  19657  odbezout  19802  odeq1  19804  dprddomcld  20247  dvreq1  20671  unitrrg  20985  frgpcyg  21909  obslbs  22066  coe1tm  22622  matunitlindflem2  23025  tgss3  23334  uptx  23974  txindislem  23982  qtopeu  24065  hmeocnvb  24123  qtophmeo  24166  trufil  24259  ufinffr  24278  ghmcnp  24464  tgioo  25145  lmmcvg  25612  bcth3  25682  ovolunlem1a  25847  vitali  25964  ismbf  25979  ismbfcn  25980  rolle  26340  itgsubstlem  26398  vieta1lem2  26664  elqaalem3  26674  aacjcl  26684  efif1olem4  26903  lognegb  26948  logcj  26964  argimgt0  26970  logdmnrp  26999  logcnlem3  27002  logrec  27121  dcubic  27204  isppw  27471  rplogsumlem2  27842  pntpbnd1  27943  ltsres  28049  nosupno  28090  nosupres  28094  noinfno  28105  noinfres  28109  negs11  28465  divsmo  28600  n0subs  28779  n0ltsp1le  28781  z12negsclb  28897  axlowdimlem16  29565  usgr0vb  29848  nbgrssvwo2  29973  redwlk  30281  usgr2pthspth  30378  usgr2pth  30380  wlkswwlksf1o  30498  wlklnwwlkln2lem  30501  wpthswwlks2on  30583  clwlkclwwlkf  30629  wwlksubclwwlk  30679  frgr0v  30893  grpoinveu  31151  grpoinvf  31164  diporthcom  31348  norm1exi  31882  shmodsi  32021  shmodi  32022  dfch2  32039  orthin  32078  chssoc  32128  spansncvi  32284  kbpj  32588  lnopunilem1  32642  cnlnssadj  32712  bra11  32740  strlem4  32886  strlem5  32887  hstrlem4  32894  hstrlem5  32895  dmdmd  32932  mdslle1i  32949  mdslle2i  32950  mdslmd1lem1  32957  atcvatlem  33017  atcvat4i  33029  mdsymlem3  33037  bcm1n  33457  xmulcand  33557  xreceu  33558  tpr2rico  34614  bnj1125  35692  fnfvintima  35786  infinfnum  35849  acwer1prc  35852  revwlkb  36065  mrsubff1  36446  mvhf1  36491  funpsstri  36709  btwnintr  36962  idinside  37027  btwnconn1lem13  37042  fneval  37318  bj-equsal1t  37912  resssres  38139  relssresv  38145  bj-brrelex12ALT  38173  bj-elid6  38283  bj-isrvec2  38413  bj-bary1lem1  38424  bj-bary1  38425  fvineqsnf1  38525  wl-equsal1i  38668  poimirlem4  38734  poimirlem9  38739  ismtybndlem  38932  grpoeqdivid  39007  0rngo  39153  dmqseqim  39865  eldisjdmqsim2  39940  qmapeldisjsim  39984  rnqmapeleldisjsim  39986  ax12indalem  40194  ax12inda2ALT  40195  lcvexchlem4  40286  lcvexchlem5  40287  opcon3b  40445  2dim  40719  ps-1  40726  paddclN  41091  ltrnnid  41385  cdleme22b  41590  dihmeetlem13N  42568  dih1dimatlem  42578  dihlspsnat  42582  eqresfnbd  43479  remulcan2d  43500  log11d  43590  sn-addcand  43664  sn-addcan2d  43666  rediveud  43687  onsupneqmaxlim0  44418  sqrtcval  44833  frege58c  45113  gneispa  45322  nzss  45493  expgrowth  45511  sbiota1  45609  ormkglobd  48092  f1cof1b  48352  f1ocof1ob2  48357  fafv2elrnb  48510  sbgoldbwt  49080  dignn0flhalflem1  49932  rrxlinesc  50053  oppff1  50469  aacllem  51219