Theorem syl5ib 247

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  syl5ibcom  248  syl5ibr  249  sbft  2267  dvelimdf  2460  sb4ALT  2564  sbftALT  2569  gencl  3481  vtoclgft  3501  vtoclgftOLD  3502  spsbc  3733  ssnelpss  4039  sscon34b  4219  dfnfc2  4822  uniintsn  4875  prex  5298  copsexgw  5346  copsexg  5347  posn  5601  optocl  5609  funimass1  6406  f1ocnvb  6603  eqfnfv2  6780  elpreima  6805  fconst5  6945  dff13  6991  f1ocnvfv  7013  f1ocnvfvb  7014  fliftfun  7044  eusvobj2  7128  sorpsscmpl  7440  ssonprc  7487  xpexr  7605  xpexcnv  7607  relcnvexb  7613  dmfex  7623  frxp  7803  mpoxopn0yelv  7862  rntpos  7888  oawordeulem  8163  oalimcl  8169  odi  8188  omeulem2  8192  oeeulem  8210  erexb  8297  unxpdomlem2  8707  dif1en  8735  enp1ilem  8736  findcard2  8742  isfinite2  8760  unfi  8769  fodomfib  8782  inf0  9068  rankxplim2  9293  scott0  9299  djuexb  9322  ficardom  9374  cardaleph  9500  dfac5  9539  cflim2  9674  fin23lem23  9737  fin23lem28  9751  isf32lem5  9768  domtriomlem  9853  ac6num  9890  zorn2lem5  9911  zorn2lem6  9912  iunfo  9950  axrepndlem2  10004  axregnd  10015  hargch  10084  addcanpi  10310  mulcanpi  10311  indpi  10318  ltaddnq  10385  ltexnq  10386  prlem934  10444  ltaddpr2  10446  ltaprlem  10455  supsrlem  10522  ssxr  10699  ltxrlt  10700  addcan  10813  addcan2  10814  neg11  10926  negreb  10940  mulcand  11262  receu  11274  ldiv  11463  lemul1a  11483  cju  11621  nn1suc  11647  nnaddcl  11648  nndivtr  11672  znegclb  12007  zmulcl  12019  zeo  12056  uz11  12255  uzp1  12267  eqreznegel  12322  rpnnen1lem6  12369  xrltne  12544  xneg11  12596  xnegdi  12629  xrsupss  12690  xrinfmss  12691  elfznelfzob  13138  modadd1  13271  modmul1  13287  om2uzlti  13313  bccmpl  13665  hashen  13703  fz1eqb  13711  hashfn  13732  hashnn0n0nn  13748  hashtpg  13839  eqwrd  13900  ccatopth  14069  ccatopth2  14070  swrdccatin2  14082  cj11  14513  rennim  14590  cnpart  14591  sqrmo  14603  sqrtgt0  14610  sqreulem  14711  sqreu  14712  cnsqrt00  14744  lo1o1  14881  lo1eq  14917  rlimeq  14918  sumss  15073  cvgcmp  15163  fprodser  15295  efne0  15442  dvdsabseq  15655  divalglem8  15741  bitsinv1lem  15780  pcfac  16225  prmreclem3  16244  sectmon  17044  yoniso  17527  lublecllem  17590  oduposb  17738  mgmb1mgm1  17857  sgrp2rid2  18083  grpinveu  18130  mulgass  18256  galcan  18426  symg1bas  18511  cayleylem2  18533  odbezout  18677  odeq1  18679  dprddomcld  19116  dvreq1  19439  unitrrg  20059  frgpcyg  20265  obslbs  20419  coe1tm  20902  tgss3  21591  uptx  22230  txindislem  22238  qtopeu  22321  hmeocnvb  22379  qtophmeo  22422  trufil  22515  ufinffr  22534  ghmcnp  22720  tgioo  23401  lmmcvg  23865  bcth3  23935  ovolunlem1a  24100  vitali  24217  ismbf  24232  ismbfcn  24233  rolle  24593  itgsubstlem  24651  vieta1lem2  24907  elqaalem3  24917  aacjcl  24923  efif1olem4  25137  lognegb  25181  logcj  25197  argimgt0  25203  logdmnrp  25232  logcnlem3  25235  logrec  25349  dcubic  25432  isppw  25699  rplogsumlem2  26069  pntpbnd1  26170  axlowdimlem16  26751  usgr0vb  27027  nbgrssvwo2  27152  redwlk  27462  usgr2pthspth  27551  usgr2pth  27553  wlkswwlksf1o  27665  wlklnwwlkln2lem  27668  wpthswwlks2on  27747  clwlkclwwlkf  27793  wwlksubclwwlk  27843  frgr0v  28047  grpoinveu  28302  grpoinvf  28315  diporthcom  28499  norm1exi  29033  shmodsi  29172  shmodi  29173  dfch2  29190  orthin  29229  chssoc  29279  spansncvi  29435  kbpj  29739  lnopunilem1  29793  cnlnssadj  29863  bra11  29891  strlem4  30037  strlem5  30038  hstrlem4  30045  hstrlem5  30046  dmdmd  30083  mdslle1i  30100  mdslle2i  30101  mdslmd1lem1  30108  atcvatlem  30168  atcvat4i  30180  mdsymlem3  30188  bcm1n  30544  xmulcand  30623  xreceu  30624  tpr2rico  31265  bnj1125  32374  revwlkb  32485  umgr2cycllem  32500  mrsubff1  32874  mvhf1  32919  funpsstri  33121  sltres  33282  nosupno  33316  nosupres  33320  btwnintr  33593  idinside  33658  btwnconn1lem13  33673  fneval  33813  bj-equsal1t  34260  bj-brrelex12ALT  34483  bj-elid6  34585  bj-isrvec2  34714  bj-bary1lem1  34725  bj-bary1  34726  fvineqsnf1  34827  wl-equsal1i  34948  uncf  35036  matunitlindflem2  35054  poimirlem4  35061  poimirlem9  35066  ismtybndlem  35244  grpoeqdivid  35319  0rngo  35465  imaexALTV  35747  dmqseqim  36050  ax12indalem  36241  ax12inda2ALT  36242  lcvexchlem4  36333  lcvexchlem5  36334  opcon3b  36492  2dim  36766  ps-1  36773  paddclN  37138  ltrnnid  37432  cdleme22b  37637  dihmeetlem13N  38615  dih1dimatlem  38625  dihlspsnat  38629  remulcan2d  39464  nnaddcom  39469  sn-addcand  39556  sn-addcan2d  39558  sqrtcval  40341  frege58c  40622  gneispa  40833  nzss  41021  expgrowth  41039  sbiota1  41138  fafv2elrnb  43791  sbgoldbwt  44295  dignn0flhalflem1  45029  rrxlinesc  45149  aacllem  45329