Theorem mtbiri 676

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 665	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nel02  3451  n0i  3452  axnul  4154  intexr  4179  intnexr  4180  iin0r  4198  exmid01  4227  ordtriexmidlem  4551  ordtriexmidlem2  4552  ordtri2or2exmidlem  4558  onsucelsucexmidlem  4561  sucprcreg  4581  preleq  4587  reg3exmidlemwe  4611  dcextest  4613  nn0eln0  4652  0nelelxp  4688  canth  5871  tfrlemisucaccv  6378  nnsucuniel  6548  nndceq  6552  nndcel  6553  2dom  6859  snnen2oprc  6916  snexxph  7009  elfi2  7031  djune  7137  updjudhcoinrg  7140  omp1eomlem  7153  nnnninfeq  7187  ismkvnex  7214  mkvprop  7217  omniwomnimkv  7226  nninfwlpoimlemginf  7235  exmidfodomrlemrALT  7263  exmidaclem  7268  netap  7314  2omotaplemap  7317  elni2  7374  ltsopi  7380  ltsonq  7458  renepnf  8067  renemnf  8068  lt0ne0d  8532  sup3exmid  8976  nnne0  9010  nn0ge2m1nn  9300  nn0nepnf  9311  xrltnr  9845  pnfnlt  9853  nltmnf  9854  xrltnsym  9859  xrlttri3  9863  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xrpnfdc  9908  xrmnfdc  9909  xsubge0  9947  xposdif  9948  xleaddadd  9953  fzpreddisj  10137  fzm1  10166  exfzdc  10307  xnn0nnen  10508  xrbdtri  11419  m1exp1  12042  3prm  12266  prmdc  12268  pcgcd1  12466  pc2dvds  12468  pcmpt  12481  exmidunben  12583  unct  12599  fvprif  12926  blssioo  14713  pilem3  14918  lgsval2lem  15126  bj-charfunbi  15303  bj-intexr  15400  bj-intnexr  15401  subctctexmid  15491  nninfsellemeq  15504  exmidsbthrlem  15512