Theorem syl5ib 244

Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
syl5ib.1	⊢ (𝜑 → 𝜓)
syl5ib.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ib	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl5ib.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	biimpd 228	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	1, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl5ibcom  245  syl5ibr  246  sbft  2260  dvelimdf  2447  gencl  3476  vtoclgft  3497  spsbc  3734  ssnelpss  4052  sscon34b  4234  dfnfc2  4869  uniintsn  4925  prex  5364  copsexgw  5417  copsexg  5418  posn  5683  optocl  5692  funimass1  6545  f1ocnvb  6759  eqfnfv2  6942  elpreima  6967  fconst5  7113  dff13  7160  f1ocnvfv  7182  f1ocnvfvb  7183  fliftfun  7215  eusvobj2  7300  sorpsscmpl  7619  ssonprc  7669  dmfex  7786  xpexr  7797  xpexcnv  7799  relcnvexb  7805  frxp  7998  mpoxopn0yelv  8060  rntpos  8086  oawordeulem  8416  oalimcl  8422  odi  8441  omeulem2  8445  oeeulem  8463  nnasmo  8524  erexb  8554  findcard2  8985  unxpdomlem2  9072  dif1enALT  9094  enp1ilem  9095  findcard2OLD  9100  isfinite2  9116  unfiOLD  9125  fodomfib  9137  inf0  9423  rankxplim2  9682  scott0  9688  djuexb  9711  ficardom  9763  cardaleph  9891  dfac5  9930  cflim2  10065  fin23lem23  10128  fin23lem28  10142  isf32lem5  10159  domtriomlem  10244  ac6num  10281  zorn2lem5  10302  zorn2lem6  10303  iunfo  10341  axrepndlem2  10395  axregnd  10406  hargch  10475  addcanpi  10701  mulcanpi  10702  indpi  10709  ltaddnq  10776  ltexnq  10777  prlem934  10835  ltaddpr2  10837  ltaprlem  10846  supsrlem  10913  ssxr  11090  ltxrlt  11091  addcan  11205  addcan2  11206  neg11  11318  negreb  11332  mulcand  11654  receu  11666  ldiv  11855  lemul1a  11875  cju  12015  nn1suc  12041  nnaddcl  12042  nndivtr  12066  znegclb  12403  zmulcl  12415  zeo  12452  uz11  12653  uzp1  12665  eqreznegel  12720  rpnnen1lem6  12768  xrltne  12943  xneg11  12995  xnegdi  13028  xrsupss  13089  xrinfmss  13090  elfznelfzob  13539  modadd1  13674  modmul1  13690  om2uzlti  13716  bccmpl  14069  hashen  14107  fz1eqb  14114  hashfn  14135  hashnn0n0nn  14151  hashtpg  14244  eqwrd  14305  ccatopth  14474  ccatopth2  14475  swrdccatin2  14487  cj11  14918  rennim  14995  cnpart  14996  sqrmo  15008  sqrtgt0  15015  sqreulem  15116  sqreu  15117  cnsqrt00  15149  lo1o1  15286  lo1eq  15322  rlimeq  15323  sumss  15481  cvgcmp  15573  fprodser  15704  efne0  15851  dvdsabseq  16067  divalglem8  16154  bitsinv1lem  16193  pcfac  16645  prmreclem3  16664  sectmon  17539  yoniso  18048  oduposb  18092  lublecllem  18123  mgmb1mgm1  18384  sgrp2rid2  18610  grpinveu  18659  mulgass  18785  galcan  18955  symg1bas  19043  cayleylem2  19066  odbezout  19210  odeq1  19212  dprddomcld  19649  dvreq1  19980  unitrrg  20609  frgpcyg  20826  obslbs  20982  coe1tm  21489  tgss3  22181  uptx  22821  txindislem  22829  qtopeu  22912  hmeocnvb  22970  qtophmeo  23013  trufil  23106  ufinffr  23125  ghmcnp  23311  tgioo  24004  lmmcvg  24470  bcth3  24540  ovolunlem1a  24705  vitali  24822  ismbf  24837  ismbfcn  24838  rolle  25199  itgsubstlem  25257  vieta1lem2  25516  elqaalem3  25526  aacjcl  25532  efif1olem4  25746  lognegb  25790  logcj  25806  argimgt0  25812  logdmnrp  25841  logcnlem3  25844  logrec  25958  dcubic  26041  isppw  26308  rplogsumlem2  26678  pntpbnd1  26779  axlowdimlem16  27370  usgr0vb  27649  nbgrssvwo2  27774  redwlk  28085  usgr2pthspth  28175  usgr2pth  28177  wlkswwlksf1o  28289  wlklnwwlkln2lem  28292  wpthswwlks2on  28371  clwlkclwwlkf  28417  wwlksubclwwlk  28467  frgr0v  28671  grpoinveu  28926  grpoinvf  28939  diporthcom  29123  norm1exi  29657  shmodsi  29796  shmodi  29797  dfch2  29814  orthin  29853  chssoc  29903  spansncvi  30059  kbpj  30363  lnopunilem1  30417  cnlnssadj  30487  bra11  30515  strlem4  30661  strlem5  30662  hstrlem4  30669  hstrlem5  30670  dmdmd  30707  mdslle1i  30724  mdslle2i  30725  mdslmd1lem1  30732  atcvatlem  30792  atcvat4i  30804  mdsymlem3  30812  bcm1n  31161  xmulcand  31240  xreceu  31241  tpr2rico  31907  bnj1125  33017  revwlkb  33132  umgr2cycllem  33147  mrsubff1  33521  mvhf1  33566  funpsstri  33784  sltres  33910  nosupno  33951  nosupres  33955  noinfno  33966  noinfres  33970  btwnintr  34366  idinside  34431  btwnconn1lem13  34446  fneval  34586  bj-equsal1t  35049  bj-brrelex12ALT  35282  bj-elid6  35385  bj-isrvec2  35515  bj-bary1lem1  35526  bj-bary1  35527  fvineqsnf1  35625  wl-equsal1i  35746  uncf  35800  matunitlindflem2  35818  poimirlem4  35825  poimirlem9  35830  ismtybndlem  36008  grpoeqdivid  36083  0rngo  36229  imaexALTV  36507  dmqseqim  36810  ax12indalem  37001  ax12inda2ALT  37002  lcvexchlem4  37093  lcvexchlem5  37094  opcon3b  37252  2dim  37526  ps-1  37533  paddclN  37898  ltrnnid  38192  cdleme22b  38397  dihmeetlem13N  39375  dih1dimatlem  39385  dihlspsnat  39389  remulcan2d  40330  nnaddcom  40335  sn-addcand  40438  sn-addcan2d  40440  sqrtcval  41287  frege58c  41567  gneispa  41778  nzss  41973  expgrowth  41991  sbiota1  42090  f1cof1b  44627  f1ocof1ob2  44632  fafv2elrnb  44785  sbgoldbwt  45287  dignn0flhalflem1  46019  rrxlinesc  46139  aacllem  46563