Theorem mtbiri 717

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 2150  n0i 2285  disjsn 2441  axnul 2709  intex 2729  intnex 2730  iin0 2740  0ellim 3031  ordunisuc 3089  dflim3 3118  vtoclibr 3213  onxpdisj 3241  fn0 3605  fvprc 3721  ndmfvrcl 3746  fvopabn 3786  dfrdg2 3933  oprssdm 4042  ndmoprrcl 4046  ecelqsdm 4299  2dom 4427  sdomex 4473  sucprcreg 4600  preleq 4603  omelon 4629  rankr1 4674  rankxpsuc 4715  card1 4833  sdomsdomcard 4848  alephnbtwn2 4869  alephgeom 4882  alephval2 4902  alephval3 4903  cfsuc 4915  ltrpq 5085  ltsopr 5136  ltapr 5151  ltxrltt 5500  xrltnrt 5541  pnfnltt 5546  nltmnft 5547  xrltnsymt 5550  nltpnftt 5566  ngtmnftt 5567  nnne0t 5949  xrsupsslem 6076  xrinfmsslem 6077  xrub 6080  zneo 6200  qbtwnxr 6279  eliooret 6386  sqrlem13 6685  ivthlem7 7287  tpsex 7605  vcex 8199  nvex 8230  spwnex3 8655  efif1lem5 8734  norm1ex 9122  dmadjrnb 9830  strlem1 10177  large 10194

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