Theorem syl5ib 247

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibcom  248  syl5ibr  249  sbft  2269  dvelimdf  2448  gencl  3436  vtoclgft  3456  vtoclgftOLD  3457  spsbc  3692  ssnelpss  4000  sscon34b  4183  dfnfc2  4817  uniintsn  4872  prex  5296  copsexgw  5344  copsexg  5345  posn  5602  optocl  5610  funimass1  6415  f1ocnvb  6625  eqfnfv2  6804  elpreima  6829  fconst5  6972  dff13  7018  f1ocnvfv  7040  f1ocnvfvb  7041  fliftfun  7072  eusvobj2  7157  sorpsscmpl  7472  ssonprc  7520  dmfex  7631  xpexr  7642  xpexcnv  7644  relcnvexb  7650  frxp  7839  mpoxopn0yelv  7901  rntpos  7927  oawordeulem  8204  oalimcl  8210  odi  8229  omeulem2  8233  oeeulem  8251  erexb  8338  findcard2  8756  unxpdomlem2  8795  dif1enOLD  8821  enp1ilem  8822  findcard2OLD  8827  isfinite2  8843  unfiOLD  8852  fodomfib  8864  inf0  9150  rankxplim2  9375  scott0  9381  djuexb  9404  ficardom  9456  cardaleph  9582  dfac5  9621  cflim2  9756  fin23lem23  9819  fin23lem28  9833  isf32lem5  9850  domtriomlem  9935  ac6num  9972  zorn2lem5  9993  zorn2lem6  9994  iunfo  10032  axrepndlem2  10086  axregnd  10097  hargch  10166  addcanpi  10392  mulcanpi  10393  indpi  10400  ltaddnq  10467  ltexnq  10468  prlem934  10526  ltaddpr2  10528  ltaprlem  10537  supsrlem  10604  ssxr  10781  ltxrlt  10782  addcan  10895  addcan2  10896  neg11  11008  negreb  11022  mulcand  11344  receu  11356  ldiv  11545  lemul1a  11565  cju  11705  nn1suc  11731  nnaddcl  11732  nndivtr  11756  znegclb  12093  zmulcl  12105  zeo  12142  uz11  12342  uzp1  12354  eqreznegel  12409  rpnnen1lem6  12457  xrltne  12632  xneg11  12684  xnegdi  12717  xrsupss  12778  xrinfmss  12779  elfznelfzob  13227  modadd1  13360  modmul1  13376  om2uzlti  13402  bccmpl  13754  hashen  13792  fz1eqb  13800  hashfn  13821  hashnn0n0nn  13837  hashtpg  13930  eqwrd  13991  ccatopth  14160  ccatopth2  14161  swrdccatin2  14173  cj11  14604  rennim  14681  cnpart  14682  sqrmo  14694  sqrtgt0  14701  sqreulem  14802  sqreu  14803  cnsqrt00  14835  lo1o1  14972  lo1eq  15008  rlimeq  15009  sumss  15167  cvgcmp  15257  fprodser  15388  efne0  15535  dvdsabseq  15751  divalglem8  15838  bitsinv1lem  15877  pcfac  16328  prmreclem3  16347  sectmon  17150  yoniso  17644  lublecllem  17707  oduposb  17855  mgmb1mgm1  17974  sgrp2rid2  18200  grpinveu  18249  mulgass  18375  galcan  18545  symg1bas  18630  cayleylem2  18652  odbezout  18796  odeq1  18798  dprddomcld  19235  dvreq1  19558  unitrrg  20178  frgpcyg  20385  obslbs  20539  coe1tm  21041  tgss3  21730  uptx  22369  txindislem  22377  qtopeu  22460  hmeocnvb  22518  qtophmeo  22561  trufil  22654  ufinffr  22673  ghmcnp  22859  tgioo  23541  lmmcvg  24006  bcth3  24076  ovolunlem1a  24241  vitali  24358  ismbf  24373  ismbfcn  24374  rolle  24734  itgsubstlem  24792  vieta1lem2  25051  elqaalem3  25061  aacjcl  25067  efif1olem4  25281  lognegb  25325  logcj  25341  argimgt0  25347  logdmnrp  25376  logcnlem3  25379  logrec  25493  dcubic  25576  isppw  25843  rplogsumlem2  26213  pntpbnd1  26314  axlowdimlem16  26895  usgr0vb  27171  nbgrssvwo2  27296  redwlk  27606  usgr2pthspth  27695  usgr2pth  27697  wlkswwlksf1o  27809  wlklnwwlkln2lem  27812  wpthswwlks2on  27891  clwlkclwwlkf  27937  wwlksubclwwlk  27987  frgr0v  28191  grpoinveu  28446  grpoinvf  28459  diporthcom  28643  norm1exi  29177  shmodsi  29316  shmodi  29317  dfch2  29334  orthin  29373  chssoc  29423  spansncvi  29579  kbpj  29883  lnopunilem1  29937  cnlnssadj  30007  bra11  30035  strlem4  30181  strlem5  30182  hstrlem4  30189  hstrlem5  30190  dmdmd  30227  mdslle1i  30244  mdslle2i  30245  mdslmd1lem1  30252  atcvatlem  30312  atcvat4i  30324  mdsymlem3  30332  bcm1n  30683  xmulcand  30762  xreceu  30763  tpr2rico  31426  bnj1125  32535  revwlkb  32650  umgr2cycllem  32665  mrsubff1  33039  mvhf1  33084  funpsstri  33303  sltres  33498  nosupno  33539  nosupres  33543  noinfno  33554  noinfres  33558  btwnintr  33951  idinside  34016  btwnconn1lem13  34031  fneval  34171  bj-equsal1t  34625  bj-brrelex12ALT  34849  bj-elid6  34951  bj-isrvec2  35080  bj-bary1lem1  35091  bj-bary1  35092  fvineqsnf1  35193  wl-equsal1i  35314  uncf  35368  matunitlindflem2  35386  poimirlem4  35393  poimirlem9  35398  ismtybndlem  35576  grpoeqdivid  35651  0rngo  35797  imaexALTV  36077  dmqseqim  36380  ax12indalem  36571  ax12inda2ALT  36572  lcvexchlem4  36663  lcvexchlem5  36664  opcon3b  36822  2dim  37096  ps-1  37103  paddclN  37468  ltrnnid  37762  cdleme22b  37967  dihmeetlem13N  38945  dih1dimatlem  38955  dihlspsnat  38959  remulcan2d  39853  nnaddcom  39858  sn-addcand  39962  sn-addcan2d  39964  sqrtcval  40778  frege58c  41059  gneispa  41270  nzss  41457  expgrowth  41475  sbiota1  41574  f1cof1b  44088  fafv2elrnb  44244  sbgoldbwt  44747  dignn0flhalflem1  45479  rrxlinesc  45599  aacllem  45942