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  2304  dvelimdf  2480  ceqsal1t  3486  gencl  3495  spsbc  3756  ssnelpss  4068  sscon34b  4256  dfnfc2  4893  uniintsn  4949  prexOLD  5413  copsexgwOLD  5472  copsexg  5473  posn  5746  optocl  5754  optoclOLD  5755  funimass1  6618  f1ocnvb  6834  eqfnfv2  7026  elpreima  7053  fconst5  7204  dff13  7252  f1ocnvfv  7276  f1ocnvfvb  7277  fliftfun  7310  eusvobj2  7404  sorpsscmpl  7733  ssonprc  7784  dmfex  7900  xpexr  7913  xpexcnv  7915  relcnvexb  7921  frxp  8120  mpoxopn0yelv  8207  rntpos  8233  oawordeulem  8537  oalimcl  8543  odi  8562  omeulem2  8566  oeeulem  8585  nnasmo  8647  erexb  8718  findcard2  9147  unxpdomlem2  9215  dif1ennnALT  9235  enp1ilem  9236  isfinite2  9256  fodomfib  9286  inf0  9588  rankxplim2  9850  scott0b  9864  scott0OLD  9865  djuexb  9902  ficardom  9954  cardaleph  10080  dfac5  10119  cflim2  10253  fin23lem23  10316  fin23lem28  10330  isf32lem5  10347  domtriomlem  10432  ac6num  10469  zorn2lem5  10490  zorn2lem6  10491  iunfo  10529  axrepndlem2  10584  axregnd  10595  hargch  10664  addcanpi  10890  mulcanpi  10891  indpi  10898  ltaddnq  10965  ltexnq  10966  prlem934  11024  ltaddpr2  11026  ltaprlem  11035  supsrlem  11102  ssxr  11285  ltxrlt  11286  addcan  11400  addcan2  11401  neg11  11515  negreb  11529  mulcand  11853  receu  11865  ldiv  12055  lemul1a  12075  cju  12220  nn1suc  12261  nnaddcl  12262  nnaddcom  12266  nndivtr  12289  znegclb  12637  zmulcl  12649  zeo  12688  uz11  12893  uzp1  12905  eqreznegel  12964  rpnnen1lem6  13012  xrltne  13194  xneg11  13247  xnegdi  13280  xrsupss  13341  xrinfmss  13342  elfznelfzob  13810  modadd1  13948  modmul1  13967  om2uzlti  13993  bccmpl  14352  hashen  14390  fz1eqb  14397  hashfn  14418  hashnn0n0nn  14434  hashtpg  14529  eqwrd  14601  ccatopth  14760  ccatopth2  14761  swrdccatin2  14773  cj11  15220  rennim  15297  cnpart  15298  sqrmo  15309  sqrtgt0  15316  sqreulem  15418  sqreu  15419  cnsqrt00  15451  lo1o1  15590  lo1eq  15626  rlimeq  15627  sumss  15782  cvgcmp  15875  fprodser  16010  efne0d  16157  efne0OLD  16159  dvdsabseq  16377  divalglem8  16464  bitsinv1lem  16505  pcfac  16965  prmreclem3  16984  sectmon  17845  yoniso  18347  oduposb  18389  lublecllem  18420  chnrev  18689  mgmb1mgm1  18719  sgrp2rid2  18994  grpinveu  19047  grpinv11  19080  mulgass  19183  galcan  19380  symg1bas  19467  cayleylem2  19489  odbezout  19634  odeq1  19636  dprddomcld  20079  dvreq1  20500  unitrrg  20813  frgpcyg  21734  obslbs  21891  coe1tm  22445  tgss3  23154  uptx  23793  txindislem  23801  qtopeu  23884  hmeocnvb  23942  qtophmeo  23985  trufil  24078  ufinffr  24097  ghmcnp  24283  tgioo  24964  lmmcvg  25431  bcth3  25501  ovolunlem1a  25666  vitali  25783  ismbf  25798  ismbfcn  25799  rolle  26160  itgsubstlem  26218  vieta1lem2  26483  elqaalem3  26493  aacjcl  26501  efif1olem4  26721  lognegb  26766  logcj  26782  argimgt0  26788  logdmnrp  26817  logcnlem3  26820  logrec  26939  dcubic  27022  isppw  27289  rplogsumlem2  27660  pntpbnd1  27761  ltsres  27837  nosupno  27878  nosupres  27882  noinfno  27893  noinfres  27897  negs11  28253  divsmo  28388  n0subs  28567  n0ltsp1le  28569  z12negsclb  28685  axlowdimlem16  29318  usgr0vb  29598  nbgrssvwo2  29723  redwlk  30031  usgr2pthspth  30122  usgr2pth  30124  wlkswwlksf1o  30239  wlklnwwlkln2lem  30242  wpthswwlks2on  30324  clwlkclwwlkf  30370  wwlksubclwwlk  30420  frgr0v  30624  grpoinveu  30882  grpoinvf  30895  diporthcom  31079  norm1exi  31613  shmodsi  31752  shmodi  31753  dfch2  31770  orthin  31809  chssoc  31859  spansncvi  32015  kbpj  32319  lnopunilem1  32373  cnlnssadj  32443  bra11  32471  strlem4  32617  strlem5  32618  hstrlem4  32625  hstrlem5  32626  dmdmd  32663  mdslle1i  32680  mdslle2i  32681  mdslmd1lem1  32688  atcvatlem  32748  atcvat4i  32760  mdsymlem3  32768  bcm1n  33151  xmulcand  33251  xreceu  33252  tpr2rico  34311  bnj1125  35389  fnfvintima  35485  revwlkb  35626  umgr2cycllem  35640  mrsubff1  36014  mvhf1  36059  funpsstri  36266  btwnintr  36519  idinside  36584  btwnconn1lem13  36599  fneval  36891  bj-equsal1t  37485  bj-brrelex12ALT  37731  bj-elid6  37842  bj-isrvec2  37972  bj-bary1lem1  37983  bj-bary1  37984  fvineqsnf1  38084  wl-equsal1i  38227  uncf  38278  matunitlindflem2  38296  poimirlem4  38303  poimirlem9  38308  ismtybndlem  38485  grpoeqdivid  38560  0rngo  38706  dmqseqim  39418  eldisjdmqsim2  39493  qmapeldisjsim  39537  rnqmapeleldisjsim  39539  ax12indalem  39747  ax12inda2ALT  39748  lcvexchlem4  39839  lcvexchlem5  39840  opcon3b  39998  2dim  40272  ps-1  40279  paddclN  40644  ltrnnid  40938  cdleme22b  41143  dihmeetlem13N  42121  dih1dimatlem  42131  dihlspsnat  42135  eqresfnbd  43031  remulcan2d  43052  log11d  43135  sn-addcand  43209  sn-addcan2d  43211  rediveud  43232  onsupneqmaxlim0  43979  sqrtcval  44395  frege58c  44675  gneispa  44884  nzss  45055  expgrowth  45073  sbiota1  45172  ormkglobd  47619  f1cof1b  47842  f1ocof1ob2  47847  fafv2elrnb  48000  sbgoldbwt  48570  dignn0flhalflem1  49423  rrxlinesc  49543  oppff1  49954  aacllem  50649