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  7318  djune  7418  updjudhcoinrg  7421  omp1eomlem  7434  nnnninfeq  7468  ismkvnex  7495  mkvprop  7498  omniwomnimkv  7507  nninfwlpoimlemginf  7516  exmidfodomrlemrALT  7555  exmidaclem  7564  netap  7620  2omotaplemap  7623  elni2  7681  ltsopi  7687  ltsonq  7765  renepnf  8373  renemnf  8374  lt0ne0d  8841  sup3exmid  9287  nnne0  9332  nn0ge2m1nn  9627  nn0nepnf  9638  xrltnr  10181  pnfnlt  10189  nltmnf  10190  xrltnsym  10195  xrlttri3  10199  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xrpnfdc  10244  xrmnfdc  10245  xsubge0  10283  xposdif  10284  xleaddadd  10289  fzpreddisj  10478  fzm1  10507  exfzdc  10659  xnn0nnen  10874  hashtpglem  11298  lsw0  11352  cats1un  11493  xrbdtri  12042  m1exp1  12668  bitsfzolem  12721  bitsfzo  12722  bitsinv1lem  12728  3prm  12906  prmdc  12908  pcgcd1  13107  pc2dvds  13109  pcmpt  13122  ballotfilem4  13241  exmidunben  13317  unct  13333  fvprif  13664  blssioo  15654  pilem3  15884  perfectlem1  16113  lgsval2lem  16129  umgredgnlp  16393  clwwlkn0  16649  clwwlknnn  16653  trlsegvdegfi  16708  eupth2lem3lem4fi  16714  konigsberg  16734  bj-charfunbi  16837  bj-intexr  16934  bj-intnexr  16935  3dom  17018  subctctexmid  17030  nninfsellemeq  17057  exmidsbthrlem  17067