Theorem mtbii 718

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

Hypotheses

Ref	Expression
mtbii.min	|- -. ps
mtbii.maj	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
mtbii	|- (ph -> -. ch)

Proof of Theorem mtbii

Step	Hyp	Ref	Expression
1		mtbii.min	. 2 |- -. ps
2		mtbii.maj	. . 3 |- (ph -> (ps <-> ch))
3	2	biimprd 154	. 2 |- (ph -> (ch -> ps))
4	1, 3	mtoi 107	1 |- (ph -> -. ch)

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

This theorem is referenced by:  ssnpss 2153  noel 2288  aceq6b 4759  nd3 4959  axunndlem1 4966  axregndlem1 4973  axregndlem2 4974  axregnd 4975  axacndlem5 4982  addnidpi 5047  indpi 5053  prodgt0 5828  lt2msq 5890  vcoprne 8201  avril1 8786

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