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  2305  dvelimdf  2480  ceqsal1t  3485  gencl  3494  spsbc  3755  ssnelpss  4066  sscon34b  4253  dfnfc2  4892  uniintsn  4948  prexOLD  5412  copsexgwOLD  5471  copsexg  5472  posn  5745  optocl  5753  optoclOLD  5754  funimass1  6619  f1ocnvb  6835  eqfnfv2  7027  elpreima  7054  fconst5  7208  dff13  7254  f1ocnvfv  7282  f1ocnvfvb  7283  fliftfun  7316  eusvobj2  7408  sorpsscmpl  7738  ssonprc  7789  dmfex  7905  xpexr  7918  xpexcnv  7920  relcnvexb  7926  frxp  8127  mpoxopn0yelv  8214  rntpos  8240  oawordeulem  8544  oalimcl  8550  odi  8569  omeulem2  8573  oeeulem  8592  nnasmo  8654  erexb  8725  uncf  8873  findcard2  9162  unxpdomlem2  9230  dif1ennnALT  9250  enp1ilem  9251  isfinite2  9271  fodomfib  9301  inf0  9603  rankxplim2  9865  scott0b  9879  scott0OLD  9880  djuexb  9917  ficardom  9969  cardaleph  10095  dfac5  10134  cflim2  10268  fin23lem23  10331  fin23lem28  10345  isf32lem5  10362  domtriomlem  10447  ac6num  10484  zorn2lem5  10505  zorn2lem6  10506  iunfo  10550  axrepndlem2  10605  axregnd  10616  hargch  10685  addcanpi  10911  mulcanpi  10912  indpi  10919  ltaddnq  10986  ltexnq  10987  prlem934  11045  ltaddpr2  11047  ltaprlem  11056  supsrlem  11123  ssxr  11306  ltxrlt  11307  addcan  11421  addcan2  11422  neg11  11536  negreb  11550  mulcand  11874  receu  11886  ldiv  12076  lemul1a  12096  cju  12241  nn1suc  12282  nnaddcl  12283  nnaddcom  12287  nndivtr  12310  znegclb  12658  zmulcl  12670  zeo  12710  uz11  12915  uzp1  12927  eqreznegel  12986  rpnnen1lem6  13034  xrltne  13216  xneg11  13269  xnegdi  13302  xrsupss  13363  xrinfmss  13364  elfznelfzob  13832  modadd1  13971  modmul1  13990  om2uzlti  14016  bccmpl  14375  hashen  14413  fz1eqb  14420  hashfn  14441  hashnn0n0nn  14457  hashtpg  14552  eqwrd  14624  ccatopth  14787  ccatopth2  14788  swrdccatin2  14800  cj11  15251  rennim  15328  cnpart  15329  sqrmo  15340  sqrtgt0  15347  sqreulem  15449  sqreu  15450  cnsqrt00  15482  lo1o1  15621  lo1eq  15657  rlimeq  15658  sumss  15812  cvgcmp  15905  fprodser  16040  efne0d  16187  efne0OLD  16189  dvdsabseq  16407  divalglem8  16494  bitsinv1lem  16535  pcfac  16995  prmreclem3  17014  sectmon  17875  yoniso  18377  oduposb  18419  lublecllem  18450  chnrev  18719  mgmb1mgm1  18751  sgrp2rid2  19042  grpinveu  19102  grpinv11  19135  mulgass  19238  galcan  19435  symg1bas  19522  cayleylem2  19544  odbezout  19689  odeq1  19691  dprddomcld  20134  dvreq1  20556  unitrrg  20869  frgpcyg  21790  obslbs  21947  coe1tm  22503  matunitlindflem2  22906  tgss3  23215  uptx  23855  txindislem  23863  qtopeu  23946  hmeocnvb  24004  qtophmeo  24047  trufil  24140  ufinffr  24159  ghmcnp  24345  tgioo  25026  lmmcvg  25493  bcth3  25563  ovolunlem1a  25728  vitali  25845  ismbf  25860  ismbfcn  25861  rolle  26222  itgsubstlem  26280  vieta1lem2  26545  elqaalem3  26555  aacjcl  26563  efif1olem4  26783  lognegb  26828  logcj  26844  argimgt0  26850  logdmnrp  26879  logcnlem3  26882  logrec  27001  dcubic  27084  isppw  27351  rplogsumlem2  27722  pntpbnd1  27823  ltsres  27899  nosupno  27940  nosupres  27944  noinfno  27955  noinfres  27959  negs11  28315  divsmo  28450  n0subs  28629  n0ltsp1le  28631  z12negsclb  28747  axlowdimlem16  29415  usgr0vb  29698  nbgrssvwo2  29823  redwlk  30131  usgr2pthspth  30228  usgr2pth  30230  wlkswwlksf1o  30348  wlklnwwlkln2lem  30351  wpthswwlks2on  30433  clwlkclwwlkf  30479  wwlksubclwwlk  30529  frgr0v  30743  grpoinveu  31001  grpoinvf  31014  diporthcom  31198  norm1exi  31732  shmodsi  31871  shmodi  31872  dfch2  31889  orthin  31928  chssoc  31978  spansncvi  32134  kbpj  32438  lnopunilem1  32492  cnlnssadj  32562  bra11  32590  strlem4  32736  strlem5  32737  hstrlem4  32744  hstrlem5  32745  dmdmd  32782  mdslle1i  32799  mdslle2i  32800  mdslmd1lem1  32807  atcvatlem  32867  atcvat4i  32879  mdsymlem3  32887  bcm1n  33268  xmulcand  33368  xreceu  33369  tpr2rico  34424  bnj1125  35503  fnfvintima  35593  revwlkb  35724  mrsubff1  36095  mvhf1  36140  funpsstri  36347  btwnintr  36601  idinside  36666  btwnconn1lem13  36681  fneval  36973  bj-equsal1t  37567  bj-brrelex12ALT  37813  bj-elid6  37924  bj-isrvec2  38054  bj-bary1lem1  38065  bj-bary1  38066  fvineqsnf1  38166  wl-equsal1i  38309  poimirlem4  38375  poimirlem9  38380  ismtybndlem  38558  grpoeqdivid  38633  0rngo  38779  dmqseqim  39491  eldisjdmqsim2  39566  qmapeldisjsim  39610  rnqmapeleldisjsim  39612  ax12indalem  39820  ax12inda2ALT  39821  lcvexchlem4  39912  lcvexchlem5  39913  opcon3b  40071  2dim  40345  ps-1  40352  paddclN  40717  ltrnnid  41011  cdleme22b  41216  dihmeetlem13N  42194  dih1dimatlem  42204  dihlspsnat  42208  eqresfnbd  43104  remulcan2d  43125  log11d  43223  sn-addcand  43297  sn-addcan2d  43299  rediveud  43320  onsupneqmaxlim0  44067  sqrtcval  44483  frege58c  44763  gneispa  44972  nzss  45143  expgrowth  45161  sbiota1  45260  ormkglobd  47707  f1cof1b  47967  f1ocof1ob2  47972  fafv2elrnb  48125  sbgoldbwt  48695  dignn0flhalflem1  49547  rrxlinesc  49667  oppff1  50076  aacllem  50774