MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnib Structured version   Unicode version

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  |-  ( ph  ->  -.  ps )
sylnib.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylnib  |-  ( ph  ->  -.  ch )

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnib.2 . . 3  |-  ( ps  <->  ch )
32a1i 11 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 3mtbid 300 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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
This theorem is referenced by:  sylnibr  305  ssnelpss  3872  fr3nr  6596  omopthi  7304  inf3lem6  8048  rankxpsuc  8298  cflim2  8641  ssfin4  8688  fin23lem30  8720  isf32lem5  8735  gchhar  9055  qextlt  11406  qextle  11407  fzneuz  11763  vdwnn  14388  psgnunilem3  16390  efgredlemb  16633  gsumzsplit  16813  gsumzsplitOLD  16814  lspexchn2  17645  lspindp2l  17648  lspindp2  17649  psrlidm  17924  psrlidmOLD  17925  mplcoe1  17995  mplcoe5  17999  mplcoe2OLD  18001  evlslem1  18052  ptopn2  19951  regr1lem2  20107  rnelfmlem  20319  hauspwpwf1  20354  tsmssplit  20520  reconn  21199  itg2splitlem  22021  itg2split  22022  itg2cn  22036  wilthlem2  23208  bposlem9  23432  frgra2v  24864  hatomistici  27146  nn0min  27477  2sqcoprm  27501  qqhf  27833  hasheuni  27957  oddpwdc  28159  ballotlemimin  28310  ballotlemfrcn0  28334  efrunt  28951  dfon2lem4  29186  dfon2lem7  29189  nofulllem5  29434  nandsym1  29855  rmspecnonsq  30811  setindtr  30934  flcidc  31092  fmul01lt1lem2  31503  icccncfext  31593  stoweidlem14  31681  stoweidlem26  31693  stirlinglem5  31745  fourierdlem42  31816  fourierdlem62  31836  fourierdlem66  31840  bnj1388  33796  atbase  34716  llnbase  34935  lplnbase  34960  lvolbase  35004  dalem48  35146  lhpbase  35424  cdlemg17pq  36100  cdlemg19  36112  cdlemg21  36114  dvh3dim3N  36878
  Copyright terms: Public domain W3C validator