Theorem syl5ib 234

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  syl5ibcom  235  syl5ibr  236  dvelimdf  2335  sb4  2356  sbft  2379  gencl  3235  vtoclgft  3254  spsbc  3448  eqsbc3rOLD  3493  ssnelpss  3718  dfnfc2  4454  uniintsn  4514  prex  4909  copsexg  4956  posn  5187  optocl  5195  ordtri3OLD  5760  funimass1  5971  f1ocnvb  6150  eqfnfv2  6312  elpreima  6337  fconst5  6471  dff13  6512  f1ocnvfv  6534  f1ocnvfvb  6535  fliftfun  6562  eusvobj2  6643  sorpsscmpl  6948  ssonprc  6992  xpexr  7106  xpexcnv  7108  relcnvexb  7114  dmfex  7124  frxp  7287  mpt2xopn0yelv  7339  rntpos  7365  oawordeulem  7634  oalimcl  7640  odi  7659  omeulem2  7663  oeeulem  7681  erexb  7767  unxpdomlem2  8165  dif1en  8193  enp1ilem  8194  findcard2  8200  isfinite2  8218  unfi  8227  fodomfib  8240  inf0  8518  rankxplim2  8743  scott0  8749  ficardom  8787  cardaleph  8912  dfac5  8951  cflim2  9085  fin23lem23  9148  fin23lem28  9162  isf32lem5  9179  domtriomlem  9264  ac6num  9301  zorn2lem5  9322  zorn2lem6  9323  iunfo  9361  axrepndlem2  9415  axregnd  9426  hargch  9495  addcanpi  9721  mulcanpi  9722  indpi  9729  ltaddnq  9796  ltexnq  9797  prlem934  9855  ltaddpr2  9857  ltaprlem  9866  supsrlem  9932  ssxr  10107  ltxrlt  10108  addcan  10220  addcan2  10221  neg11  10332  negreb  10346  mulcand  10660  receu  10672  lemul1a  10877  cju  11016  nn1suc  11041  nnaddcl  11042  nndivtr  11062  znegclb  11414  zmulcl  11426  zeo  11463  uz11  11710  uzp1  11721  eqreznegel  11774  rpnnen1lem6  11819  rpnnen1OLD  11825  xrltne  11994  xneg11  12046  xnegdi  12078  xrsupss  12139  xrinfmss  12140  elfznelfzob  12574  modadd1  12707  modmul1  12723  om2uzlti  12749  bccmpl  13096  hashen  13135  fz1eqb  13145  hashfn  13164  hashnn0n0nn  13180  hashtpg  13267  eqwrd  13346  ccatopth  13470  ccatopth2  13471  swrdccatin2  13487  swrdccat3a  13494  cj11  13902  rennim  13979  cnpart  13980  sqrmo  13992  sqrtgt0  13999  sqreulem  14099  sqreu  14100  lo1o1  14263  lo1eq  14299  rlimeq  14300  sumss  14455  cvgcmp  14548  fprodser  14679  efne0  14827  dvdsabseq  15035  divalglem8  15123  bitsinv1lem  15163  pcfac  15603  prmreclem3  15622  sectmon  16442  yoniso  16925  lublecllem  16988  oduposb  17136  mgmb1mgm1  17254  sgrp2rid2  17413  grpinveu  17456  mulgass  17579  galcan  17737  symg1bas  17816  cayleylem2  17833  odbezout  17975  odeq1  17977  dprddomcld  18400  dvreq1  18693  unitrrg  19293  coe1tm  19643  frgpcyg  19922  obslbs  20074  tgss3  20790  uptx  21428  txindislem  21436  qtopeu  21519  hmeocnvb  21577  qtophmeo  21620  trufil  21714  ufinffr  21733  ghmcnp  21918  tgioo  22599  lmmcvg  23059  bcth3  23128  ovolunlem1a  23264  vitali  23382  ismbf  23397  ismbfcn  23398  rolle  23753  itgsubstlem  23811  vieta1lem2  24066  elqaalem3  24076  aacjcl  24082  efif1olem4  24291  lognegb  24336  logcj  24352  argimgt0  24358  logdmnrp  24387  logcnlem3  24390  logrec  24501  dcubic  24573  isppw  24840  rplogsumlem2  25174  pntpbnd1  25275  axlowdimlem16  25837  usgr0vb  26129  nbgrssvwo2  26261  redwlk  26569  usgr2pthspth  26658  usgr2pth  26660  wlkpwwlkf1ouspgr  26765  wlklnwwlkln2lem  26768  wwlksubclwwlks  26925  frgr0v  27125  grpoinveu  27373  grpoinvf  27386  diporthcom  27571  norm1exi  28107  shmodsi  28248  shmodi  28249  dfch2  28266  orthin  28305  chssoc  28355  spansncvi  28511  kbpj  28815  lnopunilem1  28869  cnlnssadj  28939  bra11  28967  strlem4  29113  strlem5  29114  hstrlem4  29121  hstrlem5  29122  dmdmd  29159  mdslle1i  29176  mdslle2i  29177  mdslmd1lem1  29184  atcvatlem  29244  atcvat4i  29256  mdsymlem3  29264  bcm1n  29554  xmulcand  29629  xreceu  29630  tpr2rico  29958  bnj1125  31060  mrsubff1  31411  mvhf1  31456  funpsstri  31663  sltres  31815  nosupno  31849  nosupres  31853  btwnintr  32126  idinside  32191  btwnconn1lem13  32206  fneval  32347  bj-sbftv  32763  bj-equsal1t  32809  bj-ldiv  33155  bj-bary1lem1  33161  bj-bary1  33162  wl-equsal1i  33329  uncf  33388  matunitlindflem2  33406  poimirlem4  33413  poimirlem9  33418  ismtybndlem  33605  grpoeqdivid  33680  0rngo  33826  ax12indalem  34230  ax12inda2ALT  34231  lcvexchlem4  34324  lcvexchlem5  34325  opcon3b  34483  2dim  34756  ps-1  34763  paddclN  35128  ltrnnid  35422  cdleme22b  35629  dihmeetlem13N  36608  dih1dimatlem  36618  dihlspsnat  36622  frege58c  38215  sscon34b  38317  gneispa  38428  nzss  38516  expgrowth  38534  sbiota1  38635  sbgoldbwt  41665  dignn0flhalflem1  42409  aacllem  42547