Theorem mtbiri 317

Description: An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.)

Hypotheses

Ref	Expression
mtbiri.min	|- -. ch
mtbiri.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mtbiri	|- ( ph -> -. ps )

Proof of Theorem mtbiri

Step	Hyp	Ref	Expression
1		mtbiri.min	. 2 |- -. ch
2		mtbiri.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 219	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtoi 190	1 |- ( ph -> -. ps )

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:  psstr  3711  n0i  3920  sbcel12  3983  sbcel2  3989  sbcbr123  4706  sbcbr  4707  axnul  4788  intex  4820  intnex  4821  iin0  4839  nfcvb  4898  opelopabsb  4985  0nelelxp  5145  elimasni  5492  0ellim  5787  onxpdisj  5847  ndmfvrcl  6219  canth  6608  fvmptopab  6697  brabv  6699  oprssdm  6815  ndmovrcl  6820  omelon2  7077  undefnel2  7403  tfr2b  7492  tz7.44-3  7504  omeulem1  7662  eceqoveq  7853  2dom  8029  omxpenlem  8061  domunsn  8110  disjen  8117  infensuc  8138  snnen2o  8149  elfi2  8320  en3lp  8513  preleq  8514  rankxpsuc  8745  sdomsdomcardi  8797  cardmin2  8824  pm54.43lem  8825  alephgeom  8905  alephval3  8933  pwcdadom  9038  cfsuc  9079  cflim2  9085  alephval2  9394  axunnd  9418  canthp1lem1  9474  pwxpndom2  9487  rankcf  9599  pinq  9749  adderpq  9778  mulerpq  9779  nqpr  9836  ltsopr  9854  ltapr  9867  renepnf  10087  renemnf  10088  lt0ne0d  10593  prodgt0  10868  nnne0  11053  nn0nepnf  11371  xrltnr  11953  pnfnlt  11962  nltmnf  11963  xrltnsym  11970  nltpnft  11995  ngtmnft  11997  xsubge0  12091  xmullem2  12095  xlemul1a  12118  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  fzpreddisj  12390  fzm1  12420  uzinf  12764  hashnemnf  13132  hashclb  13149  hasheq0  13154  hashnn0n0nn  13180  prprrab  13255  lsw0  13352  cats1un  13475  geolim  14601  geolim2  14602  georeclim  14603  geoisumr  14609  m1exp1  15093  bitsfzolem  15156  bitsfzo  15157  bitsinv1lem  15163  sadcp1  15177  saddisjlem  15186  smu01lem  15207  3prm  15406  pcgcd1  15581  pc2dvds  15583  pcmpt  15596  prmreclem5  15624  vdwap0  15680  setcepi  16738  oduclatb  17144  cntzrcl  17760  pmtrfrn  17878  pmtrprfval  17907  pmtrprfvalrn  17908  psgnunilem5  17914  odhash3  17991  gsumzaddlem  18321  gsumzsplit  18327  dprdcntz2  18437  0ringnnzr  19269  mplcoe1  19465  mplcoe5  19468  psrbagsn  19495  xrsdsreclblem  19792  dsmmbas2  20081  dsmmfi  20082  islindf4  20177  pmatcollpw3fi1lem1  20591  istps  20738  haust1  21156  hauspwdom  21304  kqcldsat  21536  csdfil  21698  tsmssplit  21955  dscopn  22378  htpycc  22779  pco1  22815  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  itg11  23458  bddmulibl  23605  lhop1  23777  deg1nn0clb  23850  plypf1  23968  vieta1lem2  24066  logdmn0  24386  logcnlem3  24390  fsumharmonic  24738  sqff1o  24908  perfectlem1  24954  bposlem5  25013  lgsval2lem  25032  ostth  25328  legso  25494  axlowdimlem13  25834  axlowdimlem16  25837  axlowdim1  25839  axlowdim  25841  upgrfi  25986  lfgrnloop  26020  umgredgnlp  26042  uvtxa01vtx  26298  wlkp1lem3  26572  rusgrnumwwlkl1  26863  clwwlks  26879  trlsegvdeg  27087  konigsberg  27119  ex-res  27298  norm1exi  28107  dmadjrnb  28765  strlem1  29109  largei  29126  ifeqeqx  29361  ubico  29537  dya2iocuni  30345  eulerpartlemgh  30440  ballotlem4  30560  plymulx0  30624  signswch  30638  signstfvneq0  30649  signlem0  30664  subfacp1lem1  31161  bcneg1  31622  opelco3  31678  wsuclem  31773  wsuclemOLD  31774  sltval2  31809  sltintdifex  31814  sltres  31815  nolt02o  31845  dfrdg4  32058  linedegen  32250  rankeq1o  32278  hfninf  32293  ordcmp  32446  bj-projval  32984  bj-inftyexpidisj  33097  relowlpssretop  33212  finxpreclem2  33227  finxpreclem3  33230  finxpreclem5  33232  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  mblfinlem1  33446  nel02  34097  elpadd0  35095  diophin  37336  fiphp3d  37383  expdioph  37590  wepwsolem  37612  kelac1  37633  relintabex  37887  brnonrel  37895  relexp01min  38005  iooinlbub  39723  stoweidlem34  40251  fourierdlem60  40383  fourierdlem61  40384  fmtnoinf  41448  fmtno4prmfac193  41485  fmtno4prm  41487  31prm  41512  lighneallem3  41524  lighneallem4  41527  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  spr0nelg  41726  sprsymrelfvlem  41740  dig2nn1st  42399