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  4258  intexr  4286  intnexr  4287  iin0r  4306  exmid01  4335  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  sucprcreg  4696  preleq  4702  reg3exmidlemwe  4726  dcextest  4728  nn0eln0  4767  0nelelxp  4803  canth  6036  tfrlemisucaccv  6596  nnsucuniel  6768  nndceq  6772  nndcel  6773  2dom  7093  snnen2oprc  7161  snexxph  7267  elfi2  7306  2omap  7319  djune  7419  updjudhcoinrg  7422  omp1eomlem  7435  nnnninfeq  7469  ismkvnex  7496  mkvprop  7499  omniwomnimkv  7508  nninfwlpoimlemginf  7517  exmidfodomrlemrALT  7556  exmidaclem  7565  netap  7621  2omotaplemap  7624  elni2  7682  ltsopi  7688  ltsonq  7766  renepnf  8374  renemnf  8375  lt0ne0d  8843  sup3exmid  9290  nnne0  9335  nn0ge2m1nn  9632  nn0nepnf  9643  xrltnr  10192  pnfnlt  10200  nltmnf  10201  xrltnsym  10206  xrlttri3  10210  nltpnft  10227  ngtmnft  10230  xrrebnd  10232  xrpnfdc  10255  xrmnfdc  10256  xsubge0  10294  xposdif  10295  xleaddadd  10300  fzpreddisj  10489  fzm1  10518  exfzdc  10670  xnn0nnen  10889  hashtpglem  11314  lsw0  11368  cats1un  11509  xrbdtri  12061  m1exp1  12687  bitsfzolem  12740  bitsfzo  12741  bitsinv1lem  12747  3prm  12925  prmdc  12927  pcgcd1  13130  pc2dvds  13132  pcmpt  13145  ballotfilem4  13293  exmidunben  13369  unct  13385  fvprif  13717  blssioo  15745  pilem3  15976  perfectlem1  16260  bposlem5  16276  lgsval2lem  16295  umgredgnlp  16559  clwwlkn0  16815  clwwlknnn  16819  trlsegvdegfi  16874  eupth2lem3lem4fi  16880  konigsberg  16900  bj-charfunbi  17003  bj-intexr  17100  bj-intnexr  17101  3dom  17184  subctctexmid  17196  nninfsellemeq  17223  exmidsbthrlem  17233