Theorem mtbiri 716

Description: An inference from a biconditional, similar to modus tollens.

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

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146

This theorem is referenced by:  psstr 2146  n0i 2281  disjsn 2437  axnul 2704  intex 2724  intnex 2725  iin0 2735  0ellim 3026  ordunisuc 3084  dflim3 3113  vtoclibr 3208  onxpdisj 3236  fn0 3597  fvprc 3712  ndmfvrcl 3737  fvopabn 3777  dfrdg2 3924  oprssdm 4033  ndmoprrcl 4038  ecelqsdm 4289  2dom 4414  sdomex 4459  sucprcreg 4580  preleq 4583  omelon 4609  rankr1 4654  rankxpsuc 4695  card1 4813  sdomsdomcard 4828  alephnbtwn2 4849  alephgeom 4862  alephval2 4882  alephval3 4883  cfsuc 4895  ltrpq 5065  ltsopr 5116  ltapr 5131  ltxrltt 5480  xrltnrt 5522  pnfnltt 5527  nltmnft 5528  xrltnsymt 5531  nltpnftt 5547  ngtmnftt 5548  nnne0t 5905  xrsupsslem 6031  xrinfmsslem 6032  xrub 6035  zneo 6155  zneoOLD 6156  qbtwnxr 6225  sqrlem13 6623  ivthlem7 7230  ivthlem7OLD 7239  tpsex 7555  vcex 8151  nvex 8182  spwnex3 8597  efif1lem5 8668  norm1ex 9061  dmadjrnb 9770  strlem1 10115  large 10132

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain