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  2453  ceqsal1t  3493  gencl  3502  spsbc  3778  ssnelpss  4089  sscon34b  4279  dfnfc2  4905  uniintsn  4961  prex  5407  copsexgw  5465  copsexg  5466  posn  5740  optocl  5749  funimass1  6617  f1ocnvb  6830  eqfnfv2  7021  elpreima  7047  fconst5  7197  dff13  7246  f1ocnvfv  7270  f1ocnvfvb  7271  fliftfun  7304  eusvobj2  7395  sorpsscmpl  7726  ssonprc  7779  dmfex  7899  xpexr  7912  xpexcnv  7914  relcnvexb  7920  frxp  8123  mpoxopn0yelv  8210  rntpos  8236  oawordeulem  8564  oalimcl  8570  odi  8589  omeulem2  8593  oeeulem  8611  nnasmo  8673  erexb  8742  findcard2  9176  unxpdomlem2  9257  dif1ennnALT  9281  enp1ilem  9282  isfinite2  9304  fodomfib  9339  fodomfibOLD  9341  inf0  9633  rankxplim2  9892  scott0  9898  djuexb  9921  ficardom  9973  cardaleph  10101  dfac5  10141  cflim2  10275  fin23lem23  10338  fin23lem28  10352  isf32lem5  10369  domtriomlem  10454  ac6num  10491  zorn2lem5  10512  zorn2lem6  10513  iunfo  10551  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  11302  ltxrlt  11303  addcan  11417  addcan2  11418  neg11  11532  negreb  11546  mulcand  11868  receu  11880  ldiv  12073  lemul1a  12093  cju  12234  nn1suc  12260  nnaddcl  12261  nndivtr  12285  znegclb  12627  zmulcl  12639  zeo  12677  uz11  12875  uzp1  12891  eqreznegel  12948  rpnnen1lem6  12996  xrltne  13177  xneg11  13229  xnegdi  13262  xrsupss  13323  xrinfmss  13324  elfznelfzob  13787  modadd1  13923  modmul1  13940  om2uzlti  13966  bccmpl  14325  hashen  14363  fz1eqb  14370  hashfn  14391  hashnn0n0nn  14407  hashtpg  14501  eqwrd  14573  ccatopth  14732  ccatopth2  14733  swrdccatin2  14745  cj11  15179  rennim  15256  cnpart  15257  sqrmo  15268  sqrtgt0  15275  sqreulem  15376  sqreu  15377  cnsqrt00  15409  lo1o1  15546  lo1eq  15582  rlimeq  15583  sumss  15738  cvgcmp  15830  fprodser  15963  efne0d  16111  efne0OLD  16113  dvdsabseq  16330  divalglem8  16417  bitsinv1lem  16458  pcfac  16917  prmreclem3  16936  sectmon  17793  yoniso  18295  oduposb  18337  lublecllem  18368  mgmb1mgm1  18631  sgrp2rid2  18902  grpinveu  18955  grpinv11  18988  mulgass  19092  galcan  19285  symg1bas  19370  cayleylem2  19392  odbezout  19537  odeq1  19539  dprddomcld  19982  dvreq1  20369  unitrrg  20661  frgpcyg  21532  obslbs  21688  coe1tm  22208  tgss3  22922  uptx  23561  txindislem  23569  qtopeu  23652  hmeocnvb  23710  qtophmeo  23753  trufil  23846  ufinffr  23865  ghmcnp  24051  tgioo  24733  lmmcvg  25211  bcth3  25281  ovolunlem1a  25447  vitali  25564  ismbf  25579  ismbfcn  25580  rolle  25944  itgsubstlem  26005  vieta1lem2  26269  elqaalem3  26279  aacjcl  26285  efif1olem4  26504  lognegb  26549  logcj  26565  argimgt0  26571  logdmnrp  26600  logcnlem3  26603  logrec  26723  dcubic  26806  isppw  27074  rplogsumlem2  27446  pntpbnd1  27547  sltres  27624  nosupno  27665  nosupres  27669  noinfno  27680  noinfres  27684  negs11  27998  divsmo  28127  n0subs  28277  axlowdimlem16  28882  usgr0vb  29162  nbgrssvwo2  29287  redwlk  29598  usgr2pthspth  29690  usgr2pth  29692  wlkswwlksf1o  29807  wlklnwwlkln2lem  29810  wpthswwlks2on  29889  clwlkclwwlkf  29935  wwlksubclwwlk  29985  frgr0v  30189  grpoinveu  30446  grpoinvf  30459  diporthcom  30643  norm1exi  31177  shmodsi  31316  shmodi  31317  dfch2  31334  orthin  31373  chssoc  31423  spansncvi  31579  kbpj  31883  lnopunilem1  31937  cnlnssadj  32007  bra11  32035  strlem4  32181  strlem5  32182  hstrlem4  32189  hstrlem5  32190  dmdmd  32227  mdslle1i  32244  mdslle2i  32245  mdslmd1lem1  32252  atcvatlem  32312  atcvat4i  32324  mdsymlem3  32332  bcm1n  32718  xmulcand  32841  xreceu  32842  tpr2rico  33889  bnj1125  34969  revwlkb  35094  umgr2cycllem  35108  mrsubff1  35482  mvhf1  35527  funpsstri  35729  btwnintr  35983  idinside  36048  btwnconn1lem13  36063  fneval  36316  bj-equsal1t  36786  bj-brrelex12ALT  37031  bj-elid6  37134  bj-isrvec2  37264  bj-bary1lem1  37275  bj-bary1  37276  fvineqsnf1  37374  wl-equsal1i  37508  uncf  37569  matunitlindflem2  37587  poimirlem4  37594  poimirlem9  37599  ismtybndlem  37776  grpoeqdivid  37851  0rngo  37997  imaexALTV  38294  dmqseqim  38620  ax12indalem  38909  ax12inda2ALT  38910  lcvexchlem4  39001  lcvexchlem5  39002  opcon3b  39160  2dim  39435  ps-1  39442  paddclN  39807  ltrnnid  40101  cdleme22b  40306  dihmeetlem13N  41284  dih1dimatlem  41294  dihlspsnat  41298  eqresfnbd  42230  remulcan2d  42255  nnaddcom  42265  log11d  42342  sn-addcand  42409  sn-addcan2d  42411  onsupneqmaxlim0  43195  sqrtcval  43612  frege58c  43892  gneispa  44101  nzss  44289  expgrowth  44307  sbiota1  44406  ormkglobd  46852  f1cof1b  47054  f1ocof1ob2  47059  fafv2elrnb  47212  sbgoldbwt  47739  dignn0flhalflem1  48543  rrxlinesc  48663  aacllem  49613