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  2276  dvelimdf  2453  ceqsal1t  3473  gencl  3482  spsbc  3753  ssnelpss  4066  sscon34b  4256  dfnfc2  4885  uniintsn  4940  prex  5382  copsexgw  5438  copsexg  5439  posn  5710  optocl  5718  optoclOLD  5719  funimass1  6574  f1ocnvb  6787  eqfnfv2  6977  elpreima  7003  fconst5  7152  dff13  7200  f1ocnvfv  7224  f1ocnvfvb  7225  fliftfun  7258  eusvobj2  7350  sorpsscmpl  7679  ssonprc  7732  dmfex  7847  xpexr  7860  xpexcnv  7862  relcnvexb  7868  frxp  8068  mpoxopn0yelv  8155  rntpos  8181  oawordeulem  8481  oalimcl  8487  odi  8506  omeulem2  8510  oeeulem  8529  nnasmo  8591  erexb  8660  findcard2  9089  unxpdomlem2  9157  dif1ennnALT  9177  enp1ilem  9178  isfinite2  9198  fodomfib  9229  fodomfibOLD  9231  inf0  9530  rankxplim2  9792  scott0  9798  djuexb  9821  ficardom  9873  cardaleph  9999  dfac5  10039  cflim2  10173  fin23lem23  10236  fin23lem28  10250  isf32lem5  10267  domtriomlem  10352  ac6num  10389  zorn2lem5  10410  zorn2lem6  10411  iunfo  10449  axrepndlem2  10504  axregnd  10515  hargch  10584  addcanpi  10810  mulcanpi  10811  indpi  10818  ltaddnq  10885  ltexnq  10886  prlem934  10944  ltaddpr2  10946  ltaprlem  10955  supsrlem  11022  ssxr  11202  ltxrlt  11203  addcan  11317  addcan2  11318  neg11  11432  negreb  11446  mulcand  11770  receu  11782  ldiv  11975  lemul1a  11995  cju  12141  nn1suc  12167  nnaddcl  12168  nndivtr  12192  znegclb  12528  zmulcl  12540  zeo  12578  uz11  12776  uzp1  12788  eqreznegel  12847  rpnnen1lem6  12895  xrltne  13077  xneg11  13130  xnegdi  13163  xrsupss  13224  xrinfmss  13225  elfznelfzob  13690  modadd1  13828  modmul1  13847  om2uzlti  13873  bccmpl  14232  hashen  14270  fz1eqb  14277  hashfn  14298  hashnn0n0nn  14314  hashtpg  14408  eqwrd  14480  ccatopth  14639  ccatopth2  14640  swrdccatin2  14652  cj11  15085  rennim  15162  cnpart  15163  sqrmo  15174  sqrtgt0  15181  sqreulem  15283  sqreu  15284  cnsqrt00  15316  lo1o1  15455  lo1eq  15491  rlimeq  15492  sumss  15647  cvgcmp  15739  fprodser  15872  efne0d  16020  efne0OLD  16022  dvdsabseq  16240  divalglem8  16327  bitsinv1lem  16368  pcfac  16827  prmreclem3  16846  sectmon  17706  yoniso  18208  oduposb  18250  lublecllem  18281  chnrev  18550  mgmb1mgm1  18580  sgrp2rid2  18851  grpinveu  18904  grpinv11  18937  mulgass  19041  galcan  19233  symg1bas  19320  cayleylem2  19342  odbezout  19487  odeq1  19489  dprddomcld  19932  dvreq1  20347  unitrrg  20636  frgpcyg  21528  obslbs  21685  coe1tm  22215  tgss3  22930  uptx  23569  txindislem  23577  qtopeu  23660  hmeocnvb  23718  qtophmeo  23761  trufil  23854  ufinffr  23873  ghmcnp  24059  tgioo  24740  lmmcvg  25217  bcth3  25287  ovolunlem1a  25453  vitali  25570  ismbf  25585  ismbfcn  25586  rolle  25950  itgsubstlem  26011  vieta1lem2  26275  elqaalem3  26285  aacjcl  26291  efif1olem4  26510  lognegb  26555  logcj  26571  argimgt0  26577  logdmnrp  26606  logcnlem3  26609  logrec  26729  dcubic  26812  isppw  27080  rplogsumlem2  27452  pntpbnd1  27553  ltsres  27630  nosupno  27671  nosupres  27675  noinfno  27686  noinfres  27690  negs11  28045  divsmo  28180  n0subs  28359  n0ltsp1le  28361  z12negsclb  28477  axlowdimlem16  29030  usgr0vb  29310  nbgrssvwo2  29435  redwlk  29744  usgr2pthspth  29835  usgr2pth  29837  wlkswwlksf1o  29952  wlklnwwlkln2lem  29955  wpthswwlks2on  30037  clwlkclwwlkf  30083  wwlksubclwwlk  30133  frgr0v  30337  grpoinveu  30594  grpoinvf  30607  diporthcom  30791  norm1exi  31325  shmodsi  31464  shmodi  31465  dfch2  31482  orthin  31521  chssoc  31571  spansncvi  31727  kbpj  32031  lnopunilem1  32085  cnlnssadj  32155  bra11  32183  strlem4  32329  strlem5  32330  hstrlem4  32337  hstrlem5  32338  dmdmd  32375  mdslle1i  32392  mdslle2i  32393  mdslmd1lem1  32400  atcvatlem  32460  atcvat4i  32472  mdsymlem3  32480  bcm1n  32875  xmulcand  33002  xreceu  33003  tpr2rico  34069  bnj1125  35148  revwlkb  35320  umgr2cycllem  35334  mrsubff1  35708  mvhf1  35753  funpsstri  35960  btwnintr  36213  idinside  36278  btwnconn1lem13  36293  fneval  36546  bj-equsal1t  37023  bj-brrelex12ALT  37268  bj-elid6  37371  bj-isrvec2  37501  bj-bary1lem1  37512  bj-bary1  37513  fvineqsnf1  37611  wl-equsal1i  37745  uncf  37796  matunitlindflem2  37814  poimirlem4  37821  poimirlem9  37826  ismtybndlem  38003  grpoeqdivid  38078  0rngo  38224  dmqseqim  38911  ax12indalem  39201  ax12inda2ALT  39202  lcvexchlem4  39293  lcvexchlem5  39294  opcon3b  39452  2dim  39726  ps-1  39733  paddclN  40098  ltrnnid  40392  cdleme22b  40597  dihmeetlem13N  41575  dih1dimatlem  41585  dihlspsnat  41589  eqresfnbd  42484  remulcan2d  42508  nnaddcom  42519  log11d  42597  sn-addcand  42671  sn-addcan2d  42673  rediveud  42694  onsupneqmaxlim0  43462  sqrtcval  43878  frege58c  44158  gneispa  44367  nzss  44554  expgrowth  44572  sbiota1  44671  ormkglobd  47115  f1cof1b  47319  f1ocof1ob2  47324  fafv2elrnb  47477  sbgoldbwt  48019  dignn0flhalflem1  48857  rrxlinesc  48977  oppff1  49389  aacllem  50042