Theorem mtbiri 539

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

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127

This theorem is referenced by:  psstr 1574  n0i 1712  zfnul 1746  disjsn 1836  0inp0 1888  intex 1986  0ellim 2285  ordunisuc 2339  dflim3 2368  vtoclibr 2451  onxpdisj 2476  fn0 2739  fvprc 2829  ndmfvrcl 2849  fvopabn 2873  oprssdm 3056  ndmoprrcl 3060  ecelqsdm 3235  map0 3268  sdomex 3315  2dom 3332  sucprcreg 3451  preleq 3454  omelon 3476  rankr1 3518  sdomsdomcard 3654  alephnbtwn2 3675  alephgeom 3687  cfsuc 3709  ltrpq 3879  ltsopr 3930  ltapr 3945  nnne0t 4444  zneo 4601  sqrlem13 4743  strlem1 5691  large 5700

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

This theorem depends on definitions:  df-bi 128

metamath.org