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  2270  dvelimdf  2471  sb4ALT  2588  sbftALT  2593  gencl  3536  vtoclgft  3555  vtoclgftOLD  3556  spsbc  3787  ssnelpss  4090  dfnfc2  4862  uniintsn  4915  prex  5335  copsexgw  5383  copsexg  5384  posn  5639  optocl  5647  funimass1  6438  f1ocnvb  6630  eqfnfv2  6805  elpreima  6830  fconst5  6970  dff13  7015  f1ocnvfv  7037  f1ocnvfvb  7038  fliftfun  7067  eusvobj2  7151  sorpsscmpl  7462  ssonprc  7509  xpexr  7625  xpexcnv  7627  relcnvexb  7633  dmfex  7643  frxp  7822  mpoxopn0yelv  7881  rntpos  7907  oawordeulem  8182  oalimcl  8188  odi  8207  omeulem2  8211  oeeulem  8229  erexb  8316  unxpdomlem2  8725  dif1en  8753  enp1ilem  8754  findcard2  8760  isfinite2  8778  unfi  8787  fodomfib  8800  inf0  9086  rankxplim2  9311  scott0  9317  djuexb  9340  ficardom  9392  cardaleph  9517  dfac5  9556  cflim2  9687  fin23lem23  9750  fin23lem28  9764  isf32lem5  9781  domtriomlem  9866  ac6num  9903  zorn2lem5  9924  zorn2lem6  9925  iunfo  9963  axrepndlem2  10017  axregnd  10028  hargch  10097  addcanpi  10323  mulcanpi  10324  indpi  10331  ltaddnq  10398  ltexnq  10399  prlem934  10457  ltaddpr2  10459  ltaprlem  10468  supsrlem  10535  ssxr  10712  ltxrlt  10713  addcan  10826  addcan2  10827  neg11  10939  negreb  10953  mulcand  11275  receu  11287  ldiv  11476  lemul1a  11496  cju  11636  nn1suc  11662  nnaddcl  11663  nndivtr  11687  znegclb  12022  zmulcl  12034  zeo  12071  uz11  12270  uzp1  12282  eqreznegel  12337  rpnnen1lem6  12384  xrltne  12559  xneg11  12611  xnegdi  12644  xrsupss  12705  xrinfmss  12706  elfznelfzob  13146  modadd1  13279  modmul1  13295  om2uzlti  13321  bccmpl  13672  hashen  13710  fz1eqb  13718  hashfn  13739  hashnn0n0nn  13755  hashtpg  13846  eqwrd  13911  ccatopth  14080  ccatopth2  14081  swrdccatin2  14093  cj11  14523  rennim  14600  cnpart  14601  sqrmo  14613  sqrtgt0  14620  sqreulem  14721  sqreu  14722  cnsqrt00  14754  lo1o1  14891  lo1eq  14927  rlimeq  14928  sumss  15083  cvgcmp  15173  fprodser  15305  efne0  15452  dvdsabseq  15665  divalglem8  15753  bitsinv1lem  15792  pcfac  16237  prmreclem3  16256  sectmon  17054  yoniso  17537  lublecllem  17600  oduposb  17748  mgmb1mgm1  17867  sgrp2rid2  18093  grpinveu  18140  mulgass  18266  galcan  18436  symg1bas  18521  cayleylem2  18543  odbezout  18687  odeq1  18689  dprddomcld  19125  dvreq1  19445  unitrrg  20068  coe1tm  20443  frgpcyg  20722  obslbs  20876  tgss3  21596  uptx  22235  txindislem  22243  qtopeu  22326  hmeocnvb  22384  qtophmeo  22427  trufil  22520  ufinffr  22539  ghmcnp  22725  tgioo  23406  lmmcvg  23866  bcth3  23936  ovolunlem1a  24099  vitali  24216  ismbf  24231  ismbfcn  24232  rolle  24589  itgsubstlem  24647  vieta1lem2  24902  elqaalem3  24912  aacjcl  24918  efif1olem4  25131  lognegb  25175  logcj  25191  argimgt0  25197  logdmnrp  25226  logcnlem3  25229  logrec  25343  dcubic  25426  isppw  25693  rplogsumlem2  26063  pntpbnd1  26164  axlowdimlem16  26745  usgr0vb  27021  nbgrssvwo2  27146  redwlk  27456  usgr2pthspth  27545  usgr2pth  27547  wlkswwlksf1o  27659  wlklnwwlkln2lem  27662  wpthswwlks2on  27742  clwlkclwwlkf  27788  wwlksubclwwlk  27839  frgr0v  28043  grpoinveu  28298  grpoinvf  28311  diporthcom  28495  norm1exi  29029  shmodsi  29168  shmodi  29169  dfch2  29186  orthin  29225  chssoc  29275  spansncvi  29431  kbpj  29735  lnopunilem1  29789  cnlnssadj  29859  bra11  29887  strlem4  30033  strlem5  30034  hstrlem4  30041  hstrlem5  30042  dmdmd  30079  mdslle1i  30096  mdslle2i  30097  mdslmd1lem1  30104  atcvatlem  30164  atcvat4i  30176  mdsymlem3  30184  bcm1n  30520  xmulcand  30599  xreceu  30600  tpr2rico  31157  bnj1125  32266  revwlkb  32374  umgr2cycllem  32389  mrsubff1  32763  mvhf1  32808  funpsstri  33010  sltres  33171  nosupno  33205  nosupres  33209  btwnintr  33482  idinside  33547  btwnconn1lem13  33562  fneval  33702  bj-equsal1t  34147  bj-brrelex12ALT  34361  bj-elid6  34464  bj-isrvec2  34583  bj-bary1lem1  34594  bj-bary1  34595  fvineqsnf1  34693  wl-equsal1i  34785  uncf  34873  matunitlindflem2  34891  poimirlem4  34898  poimirlem9  34903  ismtybndlem  35086  grpoeqdivid  35161  0rngo  35307  imaexALTV  35589  dmqseqim  35892  ax12indalem  36083  ax12inda2ALT  36084  lcvexchlem4  36175  lcvexchlem5  36176  opcon3b  36334  2dim  36608  ps-1  36615  paddclN  36980  ltrnnid  37274  cdleme22b  37479  dihmeetlem13N  38457  dih1dimatlem  38467  dihlspsnat  38471  remulcan2d  39163  nnaddcom  39168  frege58c  40274  sscon34b  40376  gneispa  40487  nzss  40656  expgrowth  40674  sbiota1  40773  fafv2elrnb  43441  sbgoldbwt  43949  dignn0flhalflem1  44682  rrxlinesc  44729  aacllem  44909