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 )

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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3526  n0i  3527  ifeqeqxdc  3684  axnul  4253  intexr  4281  intnexr  4282  iin0r  4301  exmid01  4330  ordtriexmidlem  4661  ordtriexmidlem2  4662  ordtri2or2exmidlem  4668  onsucelsucexmidlem  4671  sucprcreg  4691  preleq  4697  reg3exmidlemwe  4721  dcextest  4723  nn0eln0  4762  0nelelxp  4798  canth  6026  tfrlemisucaccv  6586  nnsucuniel  6758  nndceq  6762  nndcel  6763  2dom  7083  snnen2oprc  7151  snexxph  7257  elfi2  7296  2omap  7308  djune  7408  updjudhcoinrg  7411  omp1eomlem  7424  nnnninfeq  7458  ismkvnex  7485  mkvprop  7488  omniwomnimkv  7497  nninfwlpoimlemginf  7506  exmidfodomrlemrALT  7545  exmidaclem  7554  netap  7610  2omotaplemap  7613  elni2  7671  ltsopi  7677  ltsonq  7755  renepnf  8363  renemnf  8364  lt0ne0d  8831  sup3exmid  9277  nnne0  9311  nn0ge2m1nn  9606  nn0nepnf  9617  xrltnr  10160  pnfnlt  10168  nltmnf  10169  xrltnsym  10174  xrlttri3  10178  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xrpnfdc  10223  xrmnfdc  10224  xsubge0  10262  xposdif  10263  xleaddadd  10268  fzpreddisj  10456  fzm1  10485  exfzdc  10637  xnn0nnen  10852  hashtpglem  11276  lsw0  11330  cats1un  11471  xrbdtri  12020  m1exp1  12646  bitsfzolem  12699  bitsfzo  12700  bitsinv1lem  12706  3prm  12884  prmdc  12886  pcgcd1  13085  pc2dvds  13087  pcmpt  13100  ballotfilem4  13219  exmidunben  13295  unct  13311  fvprif  13641  blssioo  15577  pilem3  15807  perfectlem1  16027  lgsval2lem  16043  umgredgnlp  16307  clwwlkn0  16563  clwwlknnn  16567  trlsegvdegfi  16622  eupth2lem3lem4fi  16628  konigsberg  16648  bj-charfunbi  16751  bj-intexr  16848  bj-intnexr  16849  3dom  16932  subctctexmid  16944  nninfsellemeq  16962  exmidsbthrlem  16972