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  8842  sup3exmid  9289  nnne0  9334  nn0ge2m1nn  9631  nn0nepnf  9642  xrltnr  10191  pnfnlt  10199  nltmnf  10200  xrltnsym  10205  xrlttri3  10209  nltpnft  10226  ngtmnft  10229  xrrebnd  10231  xrpnfdc  10254  xrmnfdc  10255  xsubge0  10293  xposdif  10294  xleaddadd  10299  fzpreddisj  10488  fzm1  10517  exfzdc  10669  xnn0nnen  10887  hashtpglem  11312  lsw0  11366  cats1un  11507  xrbdtri  12058  m1exp1  12684  bitsfzolem  12737  bitsfzo  12738  bitsinv1lem  12744  3prm  12922  prmdc  12924  pcgcd1  13127  pc2dvds  13129  pcmpt  13142  ballotfilem4  13290  exmidunben  13366  unct  13382  fvprif  13713  blssioo  15703  pilem3  15934  perfectlem1  16197  bposlem5  16213  lgsval2lem  16227  umgredgnlp  16491  clwwlkn0  16747  clwwlknnn  16751  trlsegvdegfi  16806  eupth2lem3lem4fi  16812  konigsberg  16832  bj-charfunbi  16935  bj-intexr  17032  bj-intnexr  17033  3dom  17116  subctctexmid  17128  nninfsellemeq  17155  exmidsbthrlem  17165