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  3464  n0i  3465  axnul  4168  intexr  4193  intnexr  4194  iin0r  4212  exmid01  4241  ordtriexmidlem  4566  ordtriexmidlem2  4567  ordtri2or2exmidlem  4573  onsucelsucexmidlem  4576  sucprcreg  4596  preleq  4602  reg3exmidlemwe  4626  dcextest  4628  nn0eln0  4667  0nelelxp  4703  canth  5896  tfrlemisucaccv  6410  nnsucuniel  6580  nndceq  6584  nndcel  6585  2dom  6896  snnen2oprc  6956  snexxph  7051  elfi2  7073  djune  7179  updjudhcoinrg  7182  omp1eomlem  7195  nnnninfeq  7229  ismkvnex  7256  mkvprop  7259  omniwomnimkv  7268  nninfwlpoimlemginf  7277  exmidfodomrlemrALT  7310  exmidaclem  7319  netap  7365  2omotaplemap  7368  elni2  7426  ltsopi  7432  ltsonq  7510  renepnf  8119  renemnf  8120  lt0ne0d  8585  sup3exmid  9029  nnne0  9063  nn0ge2m1nn  9354  nn0nepnf  9365  xrltnr  9900  pnfnlt  9908  nltmnf  9909  xrltnsym  9914  xrlttri3  9918  nltpnft  9935  ngtmnft  9938  xrrebnd  9940  xrpnfdc  9963  xrmnfdc  9964  xsubge0  10002  xposdif  10003  xleaddadd  10008  fzpreddisj  10192  fzm1  10221  exfzdc  10367  xnn0nnen  10580  lsw0  11039  xrbdtri  11529  m1exp1  12154  bitsfzolem  12207  bitsfzo  12208  bitsinv1lem  12214  3prm  12392  prmdc  12394  pcgcd1  12593  pc2dvds  12595  pcmpt  12608  exmidunben  12739  unct  12755  fvprif  13117  blssioo  14967  pilem3  15197  perfectlem1  15413  lgsval2lem  15429  bj-charfunbi  15680  bj-intexr  15777  bj-intnexr  15778  2omap  15865  subctctexmid  15870  nninfsellemeq  15884  exmidsbthrlem  15894