Theorem mtbiri 686

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 144	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtoi 674	1 |- ( ph -> -. ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  nel02  3526  n0i  3527  ifeqeqxdc  3687  axnul  4260  intexr  4288  intnexr  4289  iin0r  4308  exmid01  4337  ordtriexmidlem  4668  ordtriexmidlem2  4669  ordtri2or2exmidlem  4675  onsucelsucexmidlem  4678  sucprcreg  4698  preleq  4704  reg3exmidlemwe  4728  dcextest  4730  nn0eln0  4769  0nelelxp  4805  canth  6039  tfrlemisucaccv  6601  nnsucuniel  6773  nndceq  6777  nndcel  6778  2dom  7099  snnen2oprc  7167  snexxph  7274  elfi2  7311  2omap  7324  djune  7424  updjudhcoinrg  7427  omp1eomlem  7440  nnnninfeq  7474  ismkvnex  7501  mkvprop  7504  omniwomnimkv  7513  nninfwlpoimlemginf  7522  exmidfodomrlemrALT  7561  exmidaclem  7570  netap  7626  2omotaplemap  7629  elni2  7687  ltsopi  7693  ltsonq  7771  renepnf  8379  renemnf  8380  lt0ne0d  8848  sup3exmid  9295  nnne0  9341  nn0ge2m1nn  9636  nn0nepnf  9647  xrltnr  10197  pnfnlt  10205  nltmnf  10206  xrltnsym  10211  xrlttri3  10215  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xrpnfdc  10260  xrmnfdc  10261  xsubge0  10299  xposdif  10300  xleaddadd  10305  fzpreddisj  10494  fzm1  10523  exfzdc  10675  xnn0nnen  10894  hashtpglem  11319  lsw0  11373  cats1un  11514  xrbdtri  12066  m1exp1  12692  bitsfzolem  12745  bitsfzo  12746  bitsinv1lem  12752  3prm  12930  prmdc  12932  pcgcd1  13135  pc2dvds  13137  pcmpt  13150  ballotfilem4  13298  exmidunben  13374  unct  13390  fvprif  13722  blssioo  15796  pilem3  16027  perfectlem1  16316  bposlem5  16332  lgsval2lem  16351  umgredgnlp  16615  clwwlkn0  16871  clwwlknnn  16875  trlsegvdegfi  16930  eupth2lem3lem4fi  16936  konigsberg  16956  bj-charfunbi  17059  bj-intexr  17156  bj-intnexr  17157  3dom  17240  subctctexmid  17252  nninfsellemeq  17280  exmidsbthrlem  17290