Theorem imbitrid 246

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  syl5ibcom  247  imbitrrid  248  sbft  2298  dvelimdf  2474  ceqsal1t  3480  gencl  3489  spsbc  3752  ssnelpss  4063  sscon34b  4251  dfnfc2  4881  uniintsn  4937  prexOLD  5394  copsexgwOLD  5453  copsexg  5454  posn  5726  optocl  5734  optoclOLD  5735  funimass1  6592  f1ocnvb  6809  eqfnfv2  7001  elpreima  7028  fconst5  7179  dff13  7227  f1ocnvfv  7251  f1ocnvfvb  7252  fliftfun  7285  eusvobj2  7377  sorpsscmpl  7706  ssonprc  7759  dmfex  7875  xpexr  7888  xpexcnv  7890  relcnvexb  7896  frxp  8094  mpoxopn0yelv  8181  rntpos  8207  oawordeulem  8511  oalimcl  8517  odi  8536  omeulem2  8540  oeeulem  8559  nnasmo  8621  erexb  8692  findcard2  9122  unxpdomlem2  9190  dif1ennnALT  9210  enp1ilem  9211  isfinite2  9231  fodomfib  9262  fodomfibOLD  9264  inf0  9566  rankxplim2  9828  scott0  9834  djuexb  9857  ficardom  9909  cardaleph  10035  dfac5  10075  cflim2  10210  fin23lem23  10273  fin23lem28  10287  isf32lem5  10304  domtriomlem  10389  ac6num  10426  zorn2lem5  10447  zorn2lem6  10448  iunfo  10486  axrepndlem2  10541  axregnd  10552  hargch  10621  addcanpi  10847  mulcanpi  10848  indpi  10855  ltaddnq  10922  ltexnq  10923  prlem934  10981  ltaddpr2  10983  ltaprlem  10992  supsrlem  11059  ssxr  11242  ltxrlt  11243  addcan  11357  addcan2  11358  neg11  11472  negreb  11486  mulcand  11810  receu  11822  ldiv  12015  lemul1a  12035  cju  12181  nn1suc  12222  nnaddcl  12223  nnaddcom  12227  nndivtr  12250  znegclb  12598  zmulcl  12610  zeo  12649  uz11  12854  uzp1  12866  eqreznegel  12925  rpnnen1lem6  12973  xrltne  13155  xneg11  13208  xnegdi  13241  xrsupss  13302  xrinfmss  13303  elfznelfzob  13770  modadd1  13908  modmul1  13927  om2uzlti  13953  bccmpl  14312  hashen  14350  fz1eqb  14357  hashfn  14378  hashnn0n0nn  14394  hashtpg  14488  eqwrd  14560  ccatopth  14719  ccatopth2  14720  swrdccatin2  14732  cj11  15165  rennim  15242  cnpart  15243  sqrmo  15254  sqrtgt0  15261  sqreulem  15363  sqreu  15364  cnsqrt00  15396  lo1o1  15535  lo1eq  15571  rlimeq  15572  sumss  15727  cvgcmp  15820  fprodser  15955  efne0d  16103  efne0OLD  16105  dvdsabseq  16323  divalglem8  16410  bitsinv1lem  16451  pcfac  16911  prmreclem3  16930  sectmon  17791  yoniso  18293  oduposb  18335  lublecllem  18366  chnrev  18635  mgmb1mgm1  18665  sgrp2rid2  18939  grpinveu  18992  grpinv11  19025  mulgass  19129  galcan  19320  symg1bas  19407  cayleylem2  19429  odbezout  19574  odeq1  19576  dprddomcld  20019  dvreq1  20432  unitrrg  20725  frgpcyg  21598  obslbs  21755  coe1tm  22309  tgss3  23019  uptx  23658  txindislem  23666  qtopeu  23749  hmeocnvb  23807  qtophmeo  23850  trufil  23943  ufinffr  23962  ghmcnp  24148  tgioo  24829  lmmcvg  25296  bcth3  25366  ovolunlem1a  25531  vitali  25648  ismbf  25663  ismbfcn  25664  rolle  26025  itgsubstlem  26083  vieta1lem2  26345  elqaalem3  26355  aacjcl  26361  efif1olem4  26580  lognegb  26625  logcj  26641  argimgt0  26647  logdmnrp  26676  logcnlem3  26679  logrec  26798  dcubic  26881  isppw  27148  rplogsumlem2  27519  pntpbnd1  27620  ltsres  27696  nosupno  27737  nosupres  27741  noinfno  27752  noinfres  27756  negs11  28112  divsmo  28247  n0subs  28426  n0ltsp1le  28428  z12negsclb  28544  axlowdimlem16  29097  usgr0vb  29377  nbgrssvwo2  29502  redwlk  29810  usgr2pthspth  29901  usgr2pth  29903  wlkswwlksf1o  30018  wlklnwwlkln2lem  30021  wpthswwlks2on  30103  clwlkclwwlkf  30149  wwlksubclwwlk  30199  frgr0v  30403  grpoinveu  30661  grpoinvf  30674  diporthcom  30858  norm1exi  31392  shmodsi  31531  shmodi  31532  dfch2  31549  orthin  31588  chssoc  31638  spansncvi  31794  kbpj  32098  lnopunilem1  32152  cnlnssadj  32222  bra11  32250  strlem4  32396  strlem5  32397  hstrlem4  32404  hstrlem5  32405  dmdmd  32442  mdslle1i  32459  mdslle2i  32460  mdslmd1lem1  32467  atcvatlem  32527  atcvat4i  32539  mdsymlem3  32547  bcm1n  32940  xmulcand  33052  xreceu  33053  tpr2rico  34163  bnj1125  35244  revwlkb  35424  umgr2cycllem  35438  mrsubff1  35812  mvhf1  35857  funpsstri  36064  btwnintr  36317  idinside  36382  btwnconn1lem13  36397  fneval  36660  bj-equsal1t  37255  bj-brrelex12ALT  37500  bj-elid6  37610  bj-isrvec2  37740  bj-bary1lem1  37751  bj-bary1  37752  fvineqsnf1  37852  wl-equsal1i  37995  uncf  38046  matunitlindflem2  38064  poimirlem4  38071  poimirlem9  38076  ismtybndlem  38253  grpoeqdivid  38328  0rngo  38474  dmqseqim  39188  eldisjdmqsim2  39263  qmapeldisjsim  39307  rnqmapeleldisjsim  39309  ax12indalem  39517  ax12inda2ALT  39518  lcvexchlem4  39609  lcvexchlem5  39610  opcon3b  39768  2dim  40042  ps-1  40049  paddclN  40414  ltrnnid  40708  cdleme22b  40913  dihmeetlem13N  41891  dih1dimatlem  41901  dihlspsnat  41905  eqresfnbd  42799  remulcan2d  42820  log11d  42903  sn-addcand  42977  sn-addcan2d  42979  rediveud  43000  onsupneqmaxlim0  43749  sqrtcval  44165  frege58c  44445  gneispa  44654  nzss  44841  expgrowth  44859  sbiota1  44958  ormkglobd  47399  f1cof1b  47619  f1ocof1ob2  47624  fafv2elrnb  47777  sbgoldbwt  48347  dignn0flhalflem1  49185  rrxlinesc  49305  oppff1  49717  aacllem  50370