Theorem sylnib 304

Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnib.1
sylnib.2

Assertion

Ref	Expression
sylnib

Proof of Theorem sylnib

Step	Hyp	Ref	Expression
1		sylnib.1	. 2
2		sylnib.2	. . 3
3	2	a1i 11	. 2
4	1, 3	mtbid 300	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184

This theorem is referenced by:  sylnibr  305  ssnelpss  3890  fr3nr  6615  omopthi  7325  inf3lem6  8071  rankxpsuc  8321  cflim2  8664  ssfin4  8711  fin23lem30  8743  isf32lem5  8758  gchhar  9078  qextlt  11431  qextle  11432  fzneuz  11788  vdwnn  14516  psgnunilem3  16521  efgredlemb  16764  gsumzsplit  16944  gsumzsplitOLD  16945  lspexchn2  17777  lspindp2l  17780  lspindp2  17781  psrlidm  18056  psrlidmOLD  18057  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem1  18184  ptopn2  20085  regr1lem2  20241  rnelfmlem  20453  hauspwpwf1  20488  tsmssplit  20654  reconn  21333  itg2splitlem  22155  itg2split  22156  itg2cn  22170  wilthlem2  23343  bposlem9  23567  frgra2v  24999  hatomistici  27281  nn0min  27611  2sqcoprm  27635  qqhf  27967  hasheuni  28091  oddpwdc  28293  ballotlemimin  28444  ballotlemfrcn0  28468  efrunt  29085  dfon2lem4  29218  dfon2lem7  29221  nofulllem5  29466  nandsym1  29887  rmspecnonsq  30843  setindtr  30966  flcidc  31123  fmul01lt1lem2  31579  icccncfext  31690  stoweidlem14  31796  stoweidlem26  31808  stirlinglem5  31860  fourierdlem42  31931  fourierdlem62  31951  fourierdlem66  31955  bnj1388  34089  atbase  35014  llnbase  35233  lplnbase  35258  lvolbase  35302  dalem48  35444  lhpbase  35722  cdlemg17pq  36398  cdlemg19  36410  cdlemg21  36412  dvh3dim3N  37176

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 185