Theorem mtbiri 682

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 670	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3501  n0i  3502  axnul  4219  intexr  4245  intnexr  4246  iin0r  4265  exmid01  4294  ordtriexmidlem  4623  ordtriexmidlem2  4624  ordtri2or2exmidlem  4630  onsucelsucexmidlem  4633  sucprcreg  4653  preleq  4659  reg3exmidlemwe  4683  dcextest  4685  nn0eln0  4724  0nelelxp  4760  canth  5979  tfrlemisucaccv  6534  nnsucuniel  6706  nndceq  6710  nndcel  6711  2dom  7023  snnen2oprc  7089  snexxph  7192  elfi2  7214  djune  7320  updjudhcoinrg  7323  omp1eomlem  7336  nnnninfeq  7370  ismkvnex  7397  mkvprop  7400  omniwomnimkv  7409  nninfwlpoimlemginf  7418  exmidfodomrlemrALT  7457  exmidaclem  7466  netap  7516  2omotaplemap  7519  elni2  7577  ltsopi  7583  ltsonq  7661  renepnf  8269  renemnf  8270  lt0ne0d  8735  sup3exmid  9179  nnne0  9213  nn0ge2m1nn  9506  nn0nepnf  9517  xrltnr  10058  pnfnlt  10066  nltmnf  10067  xrltnsym  10072  xrlttri3  10076  nltpnft  10093  ngtmnft  10096  xrrebnd  10098  xrpnfdc  10121  xrmnfdc  10122  xsubge0  10160  xposdif  10161  xleaddadd  10166  fzpreddisj  10351  fzm1  10380  exfzdc  10532  xnn0nnen  10745  hashtpglem  11156  lsw0  11210  cats1un  11351  xrbdtri  11899  m1exp1  12525  bitsfzolem  12578  bitsfzo  12579  bitsinv1lem  12585  3prm  12763  prmdc  12765  pcgcd1  12964  pc2dvds  12966  pcmpt  12979  exmidunben  13110  unct  13126  fvprif  13489  blssioo  15347  pilem3  15577  perfectlem1  15796  lgsval2lem  15812  umgredgnlp  16076  clwwlkn0  16332  clwwlknnn  16336  trlsegvdegfi  16391  eupth2lem3lem4fi  16397  konigsberg  16417  bj-charfunbi  16510  bj-intexr  16607  bj-intnexr  16608  3dom  16691  2omap  16698  subctctexmid  16705  nninfsellemeq  16723  exmidsbthrlem  16733