Theorem imbitrid 244

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 229	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  syl5ibcom  245  imbitrrid  246  sbft  2270  dvelimdf  2447  ceqsal1t  3471  gencl  3480  spsbc  3757  ssnelpss  4067  sscon34b  4257  dfnfc2  4883  uniintsn  4938  prex  5379  copsexgw  5437  copsexg  5438  posn  5709  optocl  5717  optoclOLD  5718  funimass1  6568  f1ocnvb  6781  eqfnfv2  6970  elpreima  6996  fconst5  7146  dff13  7195  f1ocnvfv  7219  f1ocnvfvb  7220  fliftfun  7253  eusvobj2  7345  sorpsscmpl  7674  ssonprc  7727  dmfex  7845  xpexr  7858  xpexcnv  7860  relcnvexb  7866  frxp  8066  mpoxopn0yelv  8153  rntpos  8179  oawordeulem  8479  oalimcl  8485  odi  8504  omeulem2  8508  oeeulem  8526  nnasmo  8588  erexb  8657  findcard2  9088  unxpdomlem2  9156  dif1ennnALT  9180  enp1ilem  9181  isfinite2  9203  fodomfib  9238  fodomfibOLD  9240  inf0  9536  rankxplim2  9795  scott0  9801  djuexb  9824  ficardom  9876  cardaleph  10002  dfac5  10042  cflim2  10176  fin23lem23  10239  fin23lem28  10253  isf32lem5  10270  domtriomlem  10355  ac6num  10392  zorn2lem5  10413  zorn2lem6  10414  iunfo  10452  axrepndlem2  10506  axregnd  10517  hargch  10586  addcanpi  10812  mulcanpi  10813  indpi  10820  ltaddnq  10887  ltexnq  10888  prlem934  10946  ltaddpr2  10948  ltaprlem  10957  supsrlem  11024  ssxr  11203  ltxrlt  11204  addcan  11318  addcan2  11319  neg11  11433  negreb  11447  mulcand  11771  receu  11783  ldiv  11976  lemul1a  11996  cju  12142  nn1suc  12168  nnaddcl  12169  nndivtr  12193  znegclb  12530  zmulcl  12542  zeo  12580  uz11  12778  uzp1  12794  eqreznegel  12853  rpnnen1lem6  12901  xrltne  13083  xneg11  13135  xnegdi  13168  xrsupss  13229  xrinfmss  13230  elfznelfzob  13694  modadd1  13830  modmul1  13849  om2uzlti  13875  bccmpl  14234  hashen  14272  fz1eqb  14279  hashfn  14300  hashnn0n0nn  14316  hashtpg  14410  eqwrd  14482  ccatopth  14640  ccatopth2  14641  swrdccatin2  14653  cj11  15087  rennim  15164  cnpart  15165  sqrmo  15176  sqrtgt0  15183  sqreulem  15285  sqreu  15286  cnsqrt00  15318  lo1o1  15457  lo1eq  15493  rlimeq  15494  sumss  15649  cvgcmp  15741  fprodser  15874  efne0d  16022  efne0OLD  16024  dvdsabseq  16242  divalglem8  16329  bitsinv1lem  16370  pcfac  16829  prmreclem3  16848  sectmon  17707  yoniso  18209  oduposb  18251  lublecllem  18282  mgmb1mgm1  18547  sgrp2rid2  18818  grpinveu  18871  grpinv11  18904  mulgass  19008  galcan  19201  symg1bas  19288  cayleylem2  19310  odbezout  19455  odeq1  19457  dprddomcld  19900  dvreq1  20314  unitrrg  20606  frgpcyg  21498  obslbs  21655  coe1tm  22175  tgss3  22889  uptx  23528  txindislem  23536  qtopeu  23619  hmeocnvb  23677  qtophmeo  23720  trufil  23813  ufinffr  23832  ghmcnp  24018  tgioo  24700  lmmcvg  25177  bcth3  25247  ovolunlem1a  25413  vitali  25530  ismbf  25545  ismbfcn  25546  rolle  25910  itgsubstlem  25971  vieta1lem2  26235  elqaalem3  26245  aacjcl  26251  efif1olem4  26470  lognegb  26515  logcj  26531  argimgt0  26537  logdmnrp  26566  logcnlem3  26569  logrec  26689  dcubic  26772  isppw  27040  rplogsumlem2  27412  pntpbnd1  27513  sltres  27590  nosupno  27631  nosupres  27635  noinfno  27646  noinfres  27650  negs11  27978  divsmo  28110  n0subs  28276  n0sltp1le  28278  zs12negsclb  28376  axlowdimlem16  28920  usgr0vb  29200  nbgrssvwo2  29325  redwlk  29634  usgr2pthspth  29725  usgr2pth  29727  wlkswwlksf1o  29842  wlklnwwlkln2lem  29845  wpthswwlks2on  29924  clwlkclwwlkf  29970  wwlksubclwwlk  30020  frgr0v  30224  grpoinveu  30481  grpoinvf  30494  diporthcom  30678  norm1exi  31212  shmodsi  31351  shmodi  31352  dfch2  31369  orthin  31408  chssoc  31458  spansncvi  31614  kbpj  31918  lnopunilem1  31972  cnlnssadj  32042  bra11  32070  strlem4  32216  strlem5  32217  hstrlem4  32224  hstrlem5  32225  dmdmd  32262  mdslle1i  32279  mdslle2i  32280  mdslmd1lem1  32287  atcvatlem  32347  atcvat4i  32359  mdsymlem3  32367  bcm1n  32751  xmulcand  32874  xreceu  32875  tpr2rico  33878  bnj1125  34958  revwlkb  35098  umgr2cycllem  35112  mrsubff1  35486  mvhf1  35531  funpsstri  35738  btwnintr  35992  idinside  36057  btwnconn1lem13  36072  fneval  36325  bj-equsal1t  36795  bj-brrelex12ALT  37040  bj-elid6  37143  bj-isrvec2  37273  bj-bary1lem1  37284  bj-bary1  37285  fvineqsnf1  37383  wl-equsal1i  37517  uncf  37578  matunitlindflem2  37596  poimirlem4  37603  poimirlem9  37608  ismtybndlem  37785  grpoeqdivid  37860  0rngo  38006  dmqseqim  38633  ax12indalem  38923  ax12inda2ALT  38924  lcvexchlem4  39015  lcvexchlem5  39016  opcon3b  39174  2dim  39449  ps-1  39456  paddclN  39821  ltrnnid  40115  cdleme22b  40320  dihmeetlem13N  41298  dih1dimatlem  41308  dihlspsnat  41312  eqresfnbd  42205  remulcan2d  42230  nnaddcom  42241  log11d  42319  sn-addcand  42393  sn-addcan2d  42395  rediveud  42416  onsupneqmaxlim0  43197  sqrtcval  43614  frege58c  43894  gneispa  44103  nzss  44290  expgrowth  44308  sbiota1  44407  ormkglobd  46857  f1cof1b  47062  f1ocof1ob2  47067  fafv2elrnb  47220  sbgoldbwt  47762  dignn0flhalflem1  48588  rrxlinesc  48708  oppff1  49121  aacllem  49774