Theorem syl5ib 233

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  syl5ibcom  234  syl5ibr  235  dvelimdf  2323  sb4  2344  sbft  2367  gencl  3208  vtoclgft  3227  spsbc  3415  eqsbc3rOLD  3460  ssnelpss  3680  dfnfc2  4390  uniintsn  4449  prex  4836  copsexg  4882  posn  5110  optocl  5118  ordtri3OLD  5677  funimass1  5885  f1ocnvb  6063  eqfnfv2  6220  elpreima  6245  fconst5  6376  dff13  6416  f1ocnvfv  6434  f1ocnvfvb  6435  fliftfun  6462  eusvobj2  6542  sorpsscmpl  6846  ssonprc  6884  xpexr  6999  xpexcnv  7001  relcnvexb  7007  dmfex  7017  frxp  7174  mpt2xopn0yelv  7226  rntpos  7252  oawordeulem  7521  oalimcl  7527  odi  7546  omeulem2  7550  oeeulem  7568  erexb  7654  unxpdomlem2  8050  dif1en  8078  enp1ilem  8079  findcard2  8085  isfinite2  8103  unfi  8112  fodomfib  8125  inf0  8401  rankxplim2  8626  scott0  8632  ficardom  8670  cardaleph  8795  dfac5  8834  cflim2  8968  fin23lem23  9031  fin23lem28  9045  isf32lem5  9062  domtriomlem  9147  ac6num  9184  zorn2lem5  9205  zorn2lem6  9206  iunfo  9240  axrepndlem2  9294  axregnd  9305  hargch  9374  addcanpi  9600  mulcanpi  9601  indpi  9608  ltaddnq  9675  ltexnq  9676  prlem934  9734  ltaddpr2  9736  ltaprlem  9745  supsrlem  9811  ssxr  9986  ltxrlt  9987  addcan  10099  addcan2  10100  neg11  10211  negreb  10225  mulcand  10539  receu  10551  lemul1a  10756  cju  10893  nn1suc  10918  nnaddcl  10919  nndivtr  10939  znegclb  11291  zmulcl  11303  zeo  11339  uz11  11586  uzp1  11597  eqreznegel  11650  rpnnen1lem6  11695  rpnnen1OLD  11701  xrltne  11870  xneg11  11920  xnegdi  11950  xrsupss  12011  xrinfmss  12012  elfznelfzob  12440  modadd1  12569  modmul1  12585  om2uzlti  12611  bccmpl  12958  hashen  12997  fz1eqb  13007  hashfn  13025  hashnn0n0nn  13041  hashtpg  13121  eqwrd  13201  ccatopth  13322  ccatopth2  13323  swrdccatin2  13338  swrdccat3a  13345  cj11  13750  rennim  13827  cnpart  13828  sqrmo  13840  sqrtgt0  13847  sqreulem  13947  sqreu  13948  lo1o1  14111  lo1eq  14147  rlimeq  14148  sumss  14302  cvgcmp  14389  fprodser  14518  efne0  14666  dvdsabseq  14873  divalglem8  14961  bitsinv1lem  15001  pcfac  15441  prmreclem3  15460  sectmon  16265  yoniso  16748  lublecllem  16811  oduposb  16959  mgmb1mgm1  17077  sgrp2rid2  17236  grpinveu  17279  mulgass  17402  galcan  17560  symg1bas  17639  cayleylem2  17656  odbezout  17798  odeq1  17800  dprddomcld  18223  dvreq1  18516  unitrrg  19114  coe1tm  19464  frgpcyg  19741  obslbs  19893  tgss3  20601  uptx  21238  txindislem  21246  qtopeu  21329  hmeocnvb  21387  qtophmeo  21430  trufil  21524  ufinffr  21543  ghmcnp  21728  tgioo  22407  lmmcvg  22867  bcth3  22936  ovolunlem1a  23071  vitali  23188  ismbf  23203  ismbfcn  23204  rolle  23557  itgsubstlem  23615  vieta1lem2  23870  elqaalem3  23880  aacjcl  23886  efif1olem4  24095  lognegb  24140  logcj  24156  argimgt0  24162  logdmnrp  24187  logcnlem3  24190  logrec  24301  dcubic  24373  isppw  24640  rplogsumlem2  24974  pntpbnd1  25075  axlowdimlem16  25637  nbgrassvwo2  25967  is2wlk  26095  wwlkn0  26217  wlkiswwlk1  26218  wlklniswwlkn1  26227  wlklniswwlkn2  26228  wwlksubclwwlk  26332  el2wlkonot  26396  frg2wot1  26584  grpoinveu  26757  grpoinvf  26770  diporthcom  26955  norm1exi  27491  shmodsi  27632  shmodi  27633  dfch2  27650  orthin  27689  chssoc  27739  spansncvi  27895  kbpj  28199  lnopunilem1  28253  cnlnssadj  28323  bra11  28351  strlem4  28497  strlem5  28498  hstrlem4  28505  hstrlem5  28506  dmdmd  28543  mdslle1i  28560  mdslle2i  28561  mdslmd1lem1  28568  atcvatlem  28628  atcvat4i  28640  mdsymlem3  28648  bcm1n  28941  xmulcand  28960  xreceu  28961  tpr2rico  29286  bnj1125  30314  mrsubff1  30665  mvhf1  30710  funpsstri  30909  sltres  31061  nofulllem1  31101  nofulllem2  31102  btwnintr  31296  idinside  31361  btwnconn1lem13  31376  fneval  31517  bj-sbftv  31951  bj-equsal1t  31997  bj-ldiv  32332  bj-bary1lem1  32338  bj-bary1  32339  wl-equsal1i  32508  uncf  32558  matunitlindflem2  32576  poimirlem4  32583  poimirlem9  32588  ismtybndlem  32775  grpoeqdivid  32850  0rngo  32996  ax12indalem  33248  ax12inda2ALT  33249  lcvexchlem4  33342  lcvexchlem5  33343  opcon3b  33501  2dim  33774  ps-1  33781  paddclN  34146  ltrnnid  34440  cdleme22b  34647  dihmeetlem13N  35626  dih1dimatlem  35636  dihlspsnat  35640  frege58c  37235  sscon34b  37337  gneispa  37448  nzss  37538  expgrowth  37556  sbiota1  37657  bgoldbwt  40199  usgr0vb  40463  nbgrssvwo2  40587  red1wlk  40881  usgr2pthspth  40968  usgr2pth  40970  1wlkpwwlkf1ouspgr  41076  1wlklnwwlkln2lem  41079  wwlksubclwwlks  41232  frgr0v  41433  frgr2wwlk1  41494  dignn0flhalflem1  42207  aacllem  42356