Theorem syl5ib 243

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  syl5ibcom  244  syl5ibr  245  sbft  2265  dvelimdf  2450  gencl  3469  vtoclgft  3490  spsbc  3732  ssnelpss  4050  sscon34b  4233  dfnfc2  4868  uniintsn  4923  prex  5358  copsexgw  5406  copsexg  5407  posn  5671  optocl  5679  funimass1  6512  f1ocnvb  6725  eqfnfv2  6904  elpreima  6929  fconst5  7075  dff13  7122  f1ocnvfv  7144  f1ocnvfvb  7145  fliftfun  7176  eusvobj2  7261  sorpsscmpl  7578  ssonprc  7627  dmfex  7741  xpexr  7752  xpexcnv  7754  relcnvexb  7760  frxp  7951  mpoxopn0yelv  8013  rntpos  8039  oawordeulem  8361  oalimcl  8367  odi  8386  omeulem2  8390  oeeulem  8408  nnasmo  8467  erexb  8497  findcard2  8912  unxpdomlem2  8989  dif1enALT  9011  enp1ilem  9012  findcard2OLD  9017  isfinite2  9033  unfiOLD  9042  fodomfib  9054  inf0  9340  rankxplim2  9622  scott0  9628  djuexb  9651  ficardom  9703  cardaleph  9829  dfac5  9868  cflim2  10003  fin23lem23  10066  fin23lem28  10080  isf32lem5  10097  domtriomlem  10182  ac6num  10219  zorn2lem5  10240  zorn2lem6  10241  iunfo  10279  axrepndlem2  10333  axregnd  10344  hargch  10413  addcanpi  10639  mulcanpi  10640  indpi  10647  ltaddnq  10714  ltexnq  10715  prlem934  10773  ltaddpr2  10775  ltaprlem  10784  supsrlem  10851  ssxr  11028  ltxrlt  11029  addcan  11142  addcan2  11143  neg11  11255  negreb  11269  mulcand  11591  receu  11603  ldiv  11792  lemul1a  11812  cju  11952  nn1suc  11978  nnaddcl  11979  nndivtr  12003  znegclb  12340  zmulcl  12352  zeo  12389  uz11  12589  uzp1  12601  eqreznegel  12656  rpnnen1lem6  12704  xrltne  12879  xneg11  12931  xnegdi  12964  xrsupss  13025  xrinfmss  13026  elfznelfzob  13474  modadd1  13609  modmul1  13625  om2uzlti  13651  bccmpl  14004  hashen  14042  fz1eqb  14050  hashfn  14071  hashnn0n0nn  14087  hashtpg  14180  eqwrd  14241  ccatopth  14410  ccatopth2  14411  swrdccatin2  14423  cj11  14854  rennim  14931  cnpart  14932  sqrmo  14944  sqrtgt0  14951  sqreulem  15052  sqreu  15053  cnsqrt00  15085  lo1o1  15222  lo1eq  15258  rlimeq  15259  sumss  15417  cvgcmp  15509  fprodser  15640  efne0  15787  dvdsabseq  16003  divalglem8  16090  bitsinv1lem  16129  pcfac  16581  prmreclem3  16600  sectmon  17475  yoniso  17984  oduposb  18028  lublecllem  18059  mgmb1mgm1  18320  sgrp2rid2  18546  grpinveu  18595  mulgass  18721  galcan  18891  symg1bas  18979  cayleylem2  19002  odbezout  19146  odeq1  19148  dprddomcld  19585  dvreq1  19916  unitrrg  20545  frgpcyg  20762  obslbs  20918  coe1tm  21425  tgss3  22117  uptx  22757  txindislem  22765  qtopeu  22848  hmeocnvb  22906  qtophmeo  22949  trufil  23042  ufinffr  23061  ghmcnp  23247  tgioo  23940  lmmcvg  24406  bcth3  24476  ovolunlem1a  24641  vitali  24758  ismbf  24773  ismbfcn  24774  rolle  25135  itgsubstlem  25193  vieta1lem2  25452  elqaalem3  25462  aacjcl  25468  efif1olem4  25682  lognegb  25726  logcj  25742  argimgt0  25748  logdmnrp  25777  logcnlem3  25780  logrec  25894  dcubic  25977  isppw  26244  rplogsumlem2  26614  pntpbnd1  26715  axlowdimlem16  27306  usgr0vb  27585  nbgrssvwo2  27710  redwlk  28020  usgr2pthspth  28109  usgr2pth  28111  wlkswwlksf1o  28223  wlklnwwlkln2lem  28226  wpthswwlks2on  28305  clwlkclwwlkf  28351  wwlksubclwwlk  28401  frgr0v  28605  grpoinveu  28860  grpoinvf  28873  diporthcom  29057  norm1exi  29591  shmodsi  29730  shmodi  29731  dfch2  29748  orthin  29787  chssoc  29837  spansncvi  29993  kbpj  30297  lnopunilem1  30351  cnlnssadj  30421  bra11  30449  strlem4  30595  strlem5  30596  hstrlem4  30603  hstrlem5  30604  dmdmd  30641  mdslle1i  30658  mdslle2i  30659  mdslmd1lem1  30666  atcvatlem  30726  atcvat4i  30738  mdsymlem3  30746  bcm1n  31095  xmulcand  31174  xreceu  31175  tpr2rico  31841  bnj1125  32951  revwlkb  33066  umgr2cycllem  33081  mrsubff1  33455  mvhf1  33500  funpsstri  33718  sltres  33844  nosupno  33885  nosupres  33889  noinfno  33900  noinfres  33904  btwnintr  34300  idinside  34365  btwnconn1lem13  34380  fneval  34520  bj-equsal1t  34984  bj-brrelex12ALT  35217  bj-elid6  35320  bj-isrvec2  35450  bj-bary1lem1  35461  bj-bary1  35462  fvineqsnf1  35560  wl-equsal1i  35681  uncf  35735  matunitlindflem2  35753  poimirlem4  35760  poimirlem9  35765  ismtybndlem  35943  grpoeqdivid  36018  0rngo  36164  imaexALTV  36444  dmqseqim  36747  ax12indalem  36938  ax12inda2ALT  36939  lcvexchlem4  37030  lcvexchlem5  37031  opcon3b  37189  2dim  37463  ps-1  37470  paddclN  37835  ltrnnid  38129  cdleme22b  38334  dihmeetlem13N  39312  dih1dimatlem  39322  dihlspsnat  39326  remulcan2d  40273  nnaddcom  40278  sn-addcand  40381  sn-addcan2d  40383  sqrtcval  41202  frege58c  41482  gneispa  41693  nzss  41888  expgrowth  41906  sbiota1  42005  f1cof1b  44520  f1ocof1ob2  44525  fafv2elrnb  44678  sbgoldbwt  45181  dignn0flhalflem1  45913  rrxlinesc  46033  aacllem  46457