Theorem syl5ib 246

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 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  syl5ibr  248  sbft  2263  dvelimdf  2465  sb4ALT  2582  sbftALT  2587  gencl  3533  vtoclgft  3552  vtoclgftOLD  3553  spsbc  3783  ssnelpss  4086  dfnfc2  4848  uniintsn  4904  prex  5323  copsexgw  5372  copsexg  5373  posn  5630  optocl  5638  funimass1  6429  f1ocnvb  6621  eqfnfv2  6796  elpreima  6821  fconst5  6961  dff13  7005  f1ocnvfv  7027  f1ocnvfvb  7028  fliftfun  7057  eusvobj2  7141  sorpsscmpl  7452  ssonprc  7499  xpexr  7615  xpexcnv  7617  relcnvexb  7623  dmfex  7633  frxp  7812  mpoxopn0yelv  7871  rntpos  7897  oawordeulem  8172  oalimcl  8178  odi  8197  omeulem2  8201  oeeulem  8219  erexb  8306  unxpdomlem2  8715  dif1en  8743  enp1ilem  8744  findcard2  8750  isfinite2  8768  unfi  8777  fodomfib  8790  inf0  9076  rankxplim2  9301  scott0  9307  djuexb  9330  ficardom  9382  cardaleph  9507  dfac5  9546  cflim2  9677  fin23lem23  9740  fin23lem28  9754  isf32lem5  9771  domtriomlem  9856  ac6num  9893  zorn2lem5  9914  zorn2lem6  9915  iunfo  9953  axrepndlem2  10007  axregnd  10018  hargch  10087  addcanpi  10313  mulcanpi  10314  indpi  10321  ltaddnq  10388  ltexnq  10389  prlem934  10447  ltaddpr2  10449  ltaprlem  10458  supsrlem  10525  ssxr  10702  ltxrlt  10703  addcan  10816  addcan2  10817  neg11  10929  negreb  10943  mulcand  11265  receu  11277  ldiv  11466  lemul1a  11486  cju  11626  nn1suc  11651  nnaddcl  11652  nndivtr  11676  znegclb  12011  zmulcl  12023  zeo  12060  uz11  12259  uzp1  12271  eqreznegel  12326  rpnnen1lem6  12373  xrltne  12548  xneg11  12600  xnegdi  12633  xrsupss  12694  xrinfmss  12695  elfznelfzob  13135  modadd1  13268  modmul1  13284  om2uzlti  13310  bccmpl  13661  hashen  13699  fz1eqb  13707  hashfn  13728  hashnn0n0nn  13744  hashtpg  13835  eqwrd  13901  ccatopth  14070  ccatopth2  14071  swrdccatin2  14083  cj11  14513  rennim  14590  cnpart  14591  sqrmo  14603  sqrtgt0  14610  sqreulem  14711  sqreu  14712  cnsqrt00  14744  lo1o1  14881  lo1eq  14917  rlimeq  14918  sumss  15073  cvgcmp  15163  fprodser  15295  efne0  15442  dvdsabseq  15655  divalglem8  15743  bitsinv1lem  15782  pcfac  16227  prmreclem3  16246  sectmon  17044  yoniso  17527  lublecllem  17590  oduposb  17738  mgmb1mgm1  17857  sgrp2rid2  18083  grpinveu  18130  mulgass  18256  galcan  18426  symg1bas  18511  cayleylem2  18533  odbezout  18677  odeq1  18679  dprddomcld  19115  dvreq1  19435  unitrrg  20058  coe1tm  20433  frgpcyg  20712  obslbs  20866  tgss3  21586  uptx  22225  txindislem  22233  qtopeu  22316  hmeocnvb  22374  qtophmeo  22417  trufil  22510  ufinffr  22529  ghmcnp  22715  tgioo  23396  lmmcvg  23856  bcth3  23926  ovolunlem1a  24089  vitali  24206  ismbf  24221  ismbfcn  24222  rolle  24579  itgsubstlem  24637  vieta1lem2  24892  elqaalem3  24902  aacjcl  24908  efif1olem4  25121  lognegb  25165  logcj  25181  argimgt0  25187  logdmnrp  25216  logcnlem3  25219  logrec  25333  dcubic  25416  isppw  25683  rplogsumlem2  26053  pntpbnd1  26154  axlowdimlem16  26735  usgr0vb  27011  nbgrssvwo2  27136  redwlk  27446  usgr2pthspth  27535  usgr2pth  27537  wlkswwlksf1o  27649  wlklnwwlkln2lem  27652  wpthswwlks2on  27732  clwlkclwwlkf  27778  wwlksubclwwlk  27829  frgr0v  28033  grpoinveu  28288  grpoinvf  28301  diporthcom  28485  norm1exi  29019  shmodsi  29158  shmodi  29159  dfch2  29176  orthin  29215  chssoc  29265  spansncvi  29421  kbpj  29725  lnopunilem1  29779  cnlnssadj  29849  bra11  29877  strlem4  30023  strlem5  30024  hstrlem4  30031  hstrlem5  30032  dmdmd  30069  mdslle1i  30086  mdslle2i  30087  mdslmd1lem1  30094  atcvatlem  30154  atcvat4i  30166  mdsymlem3  30174  bcm1n  30510  xmulcand  30590  xreceu  30591  tpr2rico  31148  bnj1125  32257  revwlkb  32365  umgr2cycllem  32380  mrsubff1  32754  mvhf1  32799  funpsstri  33001  sltres  33162  nosupno  33196  nosupres  33200  btwnintr  33473  idinside  33538  btwnconn1lem13  33553  fneval  33693  bj-equsal1t  34138  bj-brrelex12ALT  34351  bj-elid6  34454  bj-isrvec2  34573  bj-bary1lem1  34584  bj-bary1  34585  fvineqsnf1  34683  wl-equsal1i  34775  uncf  34863  matunitlindflem2  34881  poimirlem4  34888  poimirlem9  34893  ismtybndlem  35076  grpoeqdivid  35151  0rngo  35297  imaexALTV  35579  dmqseqim  35882  ax12indalem  36073  ax12inda2ALT  36074  lcvexchlem4  36165  lcvexchlem5  36166  opcon3b  36324  2dim  36598  ps-1  36605  paddclN  36970  ltrnnid  37264  cdleme22b  37469  dihmeetlem13N  38447  dih1dimatlem  38457  dihlspsnat  38461  remulcan2d  39147  nnaddcom  39152  frege58c  40258  sscon34b  40360  gneispa  40471  nzss  40640  expgrowth  40658  sbiota1  40757  fafv2elrnb  43425  sbgoldbwt  43933  dignn0flhalflem1  44666  rrxlinesc  44713  aacllem  44893