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  4042  sscon34b  4249  dfnfc2  4888  uniintsn  4944  prexOLD  5400  copsexgwOLD  5460  copsexg  5461  posn  5736  optocl  5744  optoclOLD  5745  funimass1  6622  f1ocnvb  6838  eqfnfv2  7030  elpreima  7057  fconst5  7212  dff13  7258  f1ocnvfv  7286  f1ocnvfvb  7287  fliftfun  7320  eusvobj2  7412  sorpsscmpl  7750  ssonprc  7801  dmfex  7917  xpexr  7930  xpexcnv  7932  relcnvexb  7938  frxp  8138  mpoxopn0yelv  8231  rntpos  8257  oawordeulem  8563  oalimcl  8569  odi  8588  omeulem2  8592  oeeulem  8611  nnasmo  8673  erexb  8744  uncf  8892  findcard2  9181  unxpdomlem2  9249  dif1ennnALT  9269  enp1ilem  9270  isfinite2  9291  fodomfib  9321  inf0  9623  rankxplim2  9898  scott0b  9938  scott0OLD  9939  djuexb  9991  ficardom  10043  cardaleph  10169  dfac5  10208  cflim2  10342  fin23lem23  10405  fin23lem28  10419  isf32lem5  10436  domtriomlem  10521  ac6num  10558  zorn2lem5  10579  zorn2lem6  10580  iunfo  10624  axrepndlem2  10679  axregnd  10690  hargch  10759  addcanpi  10985  mulcanpi  10986  indpi  10993  ltaddnq  11060  ltexnq  11061  prlem934  11119  ltaddpr2  11121  ltaprlem  11130  supsrlem  11197  ssxr  11380  ltxrlt  11381  addcan  11495  addcan2  11496  neg11  11610  negreb  11624  mulcand  11950  receu  11962  ldiv  12152  lemul1a  12172  cju  12317  nn1suc  12358  nnaddcl  12359  nnaddcom  12363  nndivtr  12386  znegclb  12734  zmulcl  12746  zeo  12786  uz11  12991  uzp1  13003  eqreznegel  13062  rpnnen1lem6  13111  xrltne  13293  xneg11  13346  xnegdi  13379  xrsupss  13440  xrinfmss  13441  elfznelfzob  13910  modadd1  14049  modmul1  14068  om2uzlti  14094  bccmpl  14454  hashen  14492  fz1eqb  14499  hashfn  14520  hashnn0n0nn  14536  hashtpg  14631  eqwrd  14703  ccatopth  14866  ccatopth2  14867  swrdccatin2  14879  cj11  15330  rennim  15407  cnpart  15408  sqrmo  15419  sqrtgt0  15426  sqreulem  15528  sqreu  15529  cnsqrt00  15561  lo1o1  15700  lo1eq  15736  rlimeq  15737  sumss  15891  cvgcmp  15984  fprodser  16117  efne0d  16264  efne0OLD  16266  dvdsabseq  16484  divalglem8  16571  bitsinv1lem  16612  pcfac  17078  prmreclem3  17097  sectmon  17958  yoniso  18460  oduposb  18502  lublecllem  18533  chnrev  18802  mgmb1mgm1  18834  sgrp2rid2  19126  grpinveu  19186  grpinv11  19219  mulgass  19322  galcan  19519  symg1bas  19606  cayleylem2  19628  odbezout  19773  odeq1  19775  dprddomcld  20218  dvreq1  20642  unitrrg  20956  frgpcyg  21880  obslbs  22037  coe1tm  22593  matunitlindflem2  22996  tgss3  23305  uptx  23945  txindislem  23953  qtopeu  24036  hmeocnvb  24094  qtophmeo  24137  trufil  24230  ufinffr  24249  ghmcnp  24435  tgioo  25116  lmmcvg  25583  bcth3  25653  ovolunlem1a  25818  vitali  25935  ismbf  25950  ismbfcn  25951  rolle  26311  itgsubstlem  26369  vieta1lem2  26635  elqaalem3  26645  aacjcl  26655  efif1olem4  26874  lognegb  26919  logcj  26935  argimgt0  26941  logdmnrp  26970  logcnlem3  26973  logrec  27092  dcubic  27175  isppw  27442  rplogsumlem2  27813  pntpbnd1  27914  ltsres  28020  nosupno  28061  nosupres  28065  noinfno  28076  noinfres  28080  negs11  28436  divsmo  28571  n0subs  28750  n0ltsp1le  28752  z12negsclb  28868  axlowdimlem16  29536  usgr0vb  29819  nbgrssvwo2  29944  redwlk  30252  usgr2pthspth  30349  usgr2pth  30351  wlkswwlksf1o  30469  wlklnwwlkln2lem  30472  wpthswwlks2on  30554  clwlkclwwlkf  30600  wwlksubclwwlk  30650  frgr0v  30864  grpoinveu  31122  grpoinvf  31135  diporthcom  31319  norm1exi  31853  shmodsi  31992  shmodi  31993  dfch2  32010  orthin  32049  chssoc  32099  spansncvi  32255  kbpj  32559  lnopunilem1  32613  cnlnssadj  32683  bra11  32711  strlem4  32857  strlem5  32858  hstrlem4  32865  hstrlem5  32866  dmdmd  32903  mdslle1i  32920  mdslle2i  32921  mdslmd1lem1  32928  atcvatlem  32988  atcvat4i  33000  mdsymlem3  33008  bcm1n  33430  xmulcand  33530  xreceu  33531  tpr2rico  34587  bnj1125  35665  fnfvintima  35757  infinfnum  35806  acwer1prc  35809  revwlkb  35977  mrsubff1  36348  mvhf1  36393  funpsstri  36606  btwnintr  36859  idinside  36924  btwnconn1lem13  36939  fneval  37215  bj-equsal1t  37809  bj-brrelex12ALT  38057  bj-elid6  38167  bj-isrvec2  38297  bj-bary1lem1  38308  bj-bary1  38309  fvineqsnf1  38409  wl-equsal1i  38552  poimirlem4  38618  poimirlem9  38623  ismtybndlem  38816  grpoeqdivid  38891  0rngo  39037  dmqseqim  39749  eldisjdmqsim2  39824  qmapeldisjsim  39868  rnqmapeleldisjsim  39870  ax12indalem  40078  ax12inda2ALT  40079  lcvexchlem4  40170  lcvexchlem5  40171  opcon3b  40329  2dim  40603  ps-1  40610  paddclN  40975  ltrnnid  41269  cdleme22b  41474  dihmeetlem13N  42452  dih1dimatlem  42462  dihlspsnat  42466  eqresfnbd  43362  remulcan2d  43383  log11d  43473  sn-addcand  43547  sn-addcan2d  43549  rediveud  43570  onsupneqmaxlim0  44302  sqrtcval  44717  frege58c  44997  gneispa  45206  nzss  45377  expgrowth  45395  sbiota1  45494  ormkglobd  47963  f1cof1b  48223  f1ocof1ob2  48228  fafv2elrnb  48381  sbgoldbwt  48951  dignn0flhalflem1  49803  rrxlinesc  49923  oppff1  50332  aacllem  51015