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  6600  nnsucuniel  6772  nndceq  6776  nndcel  6777  2dom  7097  snnen2oprc  7165  snexxph  7272  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  9638  nn0nepnf  9649  xrltnr  10198  pnfnlt  10206  nltmnf  10207  xrltnsym  10212  xrlttri3  10216  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xrpnfdc  10261  xrmnfdc  10262  xsubge0  10300  xposdif  10301  xleaddadd  10306  fzpreddisj  10495  fzm1  10524  exfzdc  10676  xnn0nnen  10895  hashtpglem  11320  lsw0  11374  cats1un  11515  xrbdtri  12067  m1exp1  12693  bitsfzolem  12746  bitsfzo  12747  bitsinv1lem  12753  3prm  12931  prmdc  12933  pcgcd1  13136  pc2dvds  13138  pcmpt  13151  ballotfilem4  13299  exmidunben  13375  unct  13391  fvprif  13723  blssioo  15779  pilem3  16010  perfectlem1  16299  bposlem5  16315  lgsval2lem  16334  umgredgnlp  16598  clwwlkn0  16854  clwwlknnn  16858  trlsegvdegfi  16913  eupth2lem3lem4fi  16919  konigsberg  16939  bj-charfunbi  17042  bj-intexr  17139  bj-intnexr  17140  3dom  17223  subctctexmid  17235  nninfsellemeq  17263  exmidsbthrlem  17273