Theorem mtbi 208

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

Hypotheses

Ref	Expression
mtbi.1	|- -. ph
mtbi.2	|- (ph <-> ps)

Assertion

Ref	Expression
mtbi	|- -. ps

Proof of Theorem mtbi

Step	Hyp	Ref	Expression
1		mtbi.1	. 2 |- -. ph
2		mtbi.2	. . 3 |- (ph <-> ps)
3	2	notbii 204	. 2 |- (-. ph <-> -. ps)
4	1, 3	mpbi 206	1 |- -. ps

Syntax hints:  -. wn 2   <-> wb 163

This theorem is referenced by:  vprc 3449  vnex 3451  opprc1b 3542  opthwiener 3554  0nelelxp 4067  omsdomnn 5623  alephprc 6041  unialeph 6043  sinhalfpilem 10028  fiuni 10219  fsubbas 10281  bnj1224 12999  bnj1223 13001  bnj1278 13035  bnj1305 13048  bnj1474 13151  dfon2lem7 13855  sltval2 13997  heiborlem40 15994  compne 16417

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 164

Copyright terms: Public domain