Theorem mtbiri 664

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 143	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtoi 653	1 |- ( ph -> -. ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 603  ax-in2 604

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  n0i  3363  axnul  4048  intexr  4070  intnexr  4071  iin0r  4088  exmid01  4116  ordtriexmidlem  4430  ordtriexmidlem2  4431  ordtri2or2exmidlem  4436  onsucelsucexmidlem  4439  sucprcreg  4459  preleq  4465  reg3exmidlemwe  4488  dcextest  4490  nn0eln0  4528  0nelelxp  4563  tfrlemisucaccv  6215  nnsucuniel  6384  nndceq  6388  nndcel  6389  2dom  6692  snnen2oprc  6747  snexxph  6831  elfi2  6853  djune  6956  updjudhcoinrg  6959  omp1eomlem  6972  ismkvnex  7022  mkvprop  7025  exmidfodomrlemrALT  7052  exmidaclem  7057  elni2  7115  ltsopi  7121  ltsonq  7199  renepnf  7806  renemnf  7807  lt0ne0d  8268  sup3exmid  8708  nnne0  8741  nn0ge2m1nn  9030  nn0nepnf  9041  xrltnr  9559  pnfnlt  9566  nltmnf  9567  xrltnsym  9572  xrlttri3  9576  nltpnft  9590  ngtmnft  9593  xrrebnd  9595  xrpnfdc  9618  xrmnfdc  9619  xsubge0  9657  xposdif  9658  xleaddadd  9663  fzpreddisj  9844  fzm1  9873  exfzdc  10010  xrbdtri  11038  m1exp1  11587  3prm  11798  exmidunben  11928  unct  11943  blssioo  12703  pilem3  12853  bj-intexr  13095  bj-intnexr  13096  subctctexmid  13185  nninfalllemn  13191  nninfsellemeq  13199  exmidsbthrlem  13206