Theorem sylnib 318

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

Hypotheses

Ref	Expression
sylnib.1	|- ( ph -> -. ps )
sylnib.2	|- ( ps <-> ch )

Assertion

Ref	Expression
sylnib	|- ( ph -> -. ch )

Proof of Theorem sylnib

Step	Hyp	Ref	Expression
1		sylnib.1	. 2 |- ( ph -> -. ps )
2		sylnib.2	. . 3 |- ( ps <-> ch )
3	2	a1i 11	. 2 |- ( ph -> ( ps <-> ch ) )
4	1, 3	mtbid 314	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> 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:  sylnibr  319  ssnelpss  3718  fr3nr  6979  omopthi  7737  inf3lem6  8530  rankxpsuc  8745  cflim2  9085  ssfin4  9132  fin23lem30  9164  isf32lem5  9179  gchhar  9501  qextlt  12034  qextle  12035  fzneuz  12421  vdwnn  15702  psgnunilem3  17916  efgredlemb  18159  gsumzsplit  18327  lspexchn2  19131  lspindp2l  19134  lspindp2  19135  psrlidm  19403  mplcoe1  19465  mplcoe5  19468  evlslem1  19515  ptopn2  21387  regr1lem2  21543  rnelfmlem  21756  hauspwpwf1  21791  tsmssplit  21955  reconn  22631  itg2splitlem  23515  itg2split  23516  itg2cn  23530  wilthlem2  24795  bposlem9  25017  nfrgr2v  27136  hatomistici  29221  nn0min  29567  2sqcoprm  29647  qqhf  30030  hasheuni  30147  oddpwdc  30416  ballotlemimin  30567  ballotlemfrcn0  30591  bnj1388  31101  efrunt  31590  dfon2lem4  31691  dfon2lem7  31694  nandsym1  32421  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  dalem48  35006  lhpbase  35284  cdlemg17pq  35960  cdlemg19  35972  cdlemg21  35974  dvh3dim3N  36738  rmspecnonsq  37472  setindtr  37591  flcidc  37744  fmul01lt1lem2  39817  icccncfext  40100  stoweidlem14  40231  stoweidlem26  40243  stirlinglem5  40295  fourierdlem42  40366  fourierdlem62  40385  fourierdlem66  40389  hoicvr  40762