Theorem syl5ib 236

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  syl5ibcom  237  syl5ibr  238  sbftv  2304  dvelimdf  2471  sb4  2488  sbft  2511  gencl  3453  vtoclgft  3472  spsbc  3676  ssnelpss  3945  dfnfc2  4679  uniintsn  4735  prex  5131  copsexg  5177  posn  5423  optocl  5431  funimass1  6205  f1ocnvb  6392  eqfnfv2  6562  elpreima  6587  fconst5  6728  dff13  6768  f1ocnvfv  6790  f1ocnvfvb  6791  fliftfun  6818  eusvobj2  6899  sorpsscmpl  7209  ssonprc  7254  xpexr  7369  xpexcnv  7371  relcnvexb  7377  dmfex  7387  frxp  7552  mpt2xopn0yelv  7605  rntpos  7631  oawordeulem  7902  oalimcl  7908  odi  7927  omeulem2  7931  oeeulem  7949  erexb  8035  unxpdomlem2  8435  dif1en  8463  enp1ilem  8464  findcard2  8470  isfinite2  8488  unfi  8497  fodomfib  8510  inf0  8796  rankxplim2  9021  scott0  9027  ficardom  9101  cardaleph  9226  dfac5  9265  cflim2  9401  fin23lem23  9464  fin23lem28  9478  isf32lem5  9495  domtriomlem  9580  ac6num  9617  zorn2lem5  9638  zorn2lem6  9639  iunfo  9677  axrepndlem2  9731  axregnd  9742  hargch  9811  addcanpi  10037  mulcanpi  10038  indpi  10045  ltaddnq  10112  ltexnq  10113  prlem934  10171  ltaddpr2  10173  ltaprlem  10182  supsrlem  10249  ssxr  10427  ltxrlt  10428  addcan  10540  addcan2  10541  neg11  10654  negreb  10668  mulcand  10986  receu  10998  ldiv  11186  lemul1a  11208  cju  11347  nn1suc  11374  nnaddcl  11375  nndivtr  11399  znegclb  11743  zmulcl  11755  zeo  11792  uz11  11992  uzp1  12004  eqreznegel  12058  rpnnen1lem6  12105  xrltne  12283  xneg11  12335  xnegdi  12367  xrsupss  12428  xrinfmss  12429  elfznelfzob  12870  modadd1  13003  modmul1  13019  om2uzlti  13045  bccmpl  13390  hashen  13428  fz1eqb  13436  hashfn  13455  hashnn0n0nn  13471  hashtpg  13557  eqwrd  13618  ccatopth  13805  ccatopthOLD  13806  ccatopth2  13807  swrdccatin2  13827  swrdccat3aOLD  13841  cj11  14280  rennim  14357  cnpart  14358  sqrmo  14370  sqrtgt0  14377  sqreulem  14477  sqreu  14478  lo1o1  14641  lo1eq  14677  rlimeq  14678  sumss  14833  cvgcmp  14923  fprodser  15053  efne0  15200  dvdsabseq  15413  divalglem8  15498  bitsinv1lem  15537  pcfac  15975  prmreclem3  15994  sectmon  16795  yoniso  17279  lublecllem  17342  oduposb  17490  mgmb1mgm1  17608  sgrp2rid2  17768  grpinveu  17811  mulgass  17931  galcan  18088  symg1bas  18167  cayleylem2  18184  odbezout  18327  odeq1  18329  dprddomcld  18755  dvreq1  19048  unitrrg  19655  coe1tm  20004  frgpcyg  20282  obslbs  20438  tgss3  21162  uptx  21800  txindislem  21808  qtopeu  21891  hmeocnvb  21949  qtophmeo  21992  trufil  22085  ufinffr  22104  ghmcnp  22289  tgioo  22970  lmmcvg  23430  bcth3  23500  ovolunlem1a  23663  vitali  23780  ismbf  23795  ismbfcn  23796  rolle  24153  itgsubstlem  24211  vieta1lem2  24466  elqaalem3  24476  aacjcl  24482  efif1olem4  24692  lognegb  24736  logcj  24752  argimgt0  24758  logdmnrp  24787  logcnlem3  24790  logrec  24904  dcubic  24987  isppw  25254  rplogsumlem2  25588  pntpbnd1  25689  axlowdimlem16  26257  usgr0vb  26535  nbgrssvwo2  26660  redwlk  26974  usgr2pthspth  27065  usgr2pth  27067  wlkswwlksf1o  27179  wlklnwwlkln2lem  27183  wpthswwlks2on  27291  clwlkclwwlkfOLD  27342  clwlkclwwlkf  27346  wwlksubclwwlk  27411  wwlksubclwwlkOLD  27412  frgr0v  27643  grpoinveu  27930  grpoinvf  27943  diporthcom  28127  norm1exi  28663  shmodsi  28804  shmodi  28805  dfch2  28822  orthin  28861  chssoc  28911  spansncvi  29067  kbpj  29371  lnopunilem1  29425  cnlnssadj  29495  bra11  29523  strlem4  29669  strlem5  29670  hstrlem4  29677  hstrlem5  29678  dmdmd  29715  mdslle1i  29732  mdslle2i  29733  mdslmd1lem1  29740  atcvatlem  29800  atcvat4i  29812  mdsymlem3  29820  bcm1n  30102  xmulcand  30175  xreceu  30176  tpr2rico  30504  bnj1125  31607  mrsubff1  31958  mvhf1  32003  funpsstri  32206  sltres  32355  nosupno  32389  nosupres  32393  btwnintr  32666  idinside  32731  btwnconn1lem13  32746  fneval  32886  bj-equsal1t  33334  bj-bary1lem1  33710  bj-bary1  33711  wl-equsal1i  33874  uncf  33932  matunitlindflem2  33951  poimirlem4  33958  poimirlem9  33963  ismtybndlem  34148  grpoeqdivid  34223  0rngo  34369  ax12indalem  35021  ax12inda2ALT  35022  lcvexchlem4  35113  lcvexchlem5  35114  opcon3b  35272  2dim  35546  ps-1  35553  paddclN  35918  ltrnnid  36212  cdleme22b  36417  dihmeetlem13N  37395  dih1dimatlem  37405  dihlspsnat  37409  nnaddcom  38055  frege58c  39056  sscon34b  39158  gneispa  39269  nzss  39357  expgrowth  39375  sbiota1  39475  fafv2elrnb  42138  sbgoldbwt  42496  dignn0flhalflem1  43257  rrxlinesc  43287  aacllem  43444