Theorem mtbir 192

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

Hypotheses

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

Assertion

Ref	Expression
mtbir	|- -. ph

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 |- -. ps
2		mtbir.2	. . 3 |- (ph <-> ps)
3	2	negbii 187	. 2 |- (-. ph <-> -. ps)
4	1, 3	mpbir 190	1 |- -. ph

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

This theorem is referenced by:  nemtbir 1641  ru 1938  pssirr 2146  nvelv 2713  iin0 2740  opprc1b 2796  0nelxp 3240  dmsn0 3324  dmsnsn0 3325  inelv 3362  co02 3508  imadif 3574  tz7.44lem1 3927  tz7.44-2 3929  tz7.48-3 3958  canth2 4482  rankpw 4676  zorn 4789  brdom3 4793  cfsuc 4907  0npq 5042  1pr 5109  0nsr 5180  0ncn 5243  ax1ne0 5272  pnfnre 5488  mnfnre 5489  xrltnrt 5533  nn0subt 6149  sqr2irr 6715  inelr 6721  climubi 7138  eirr 7379  ruclem35 7529  ruclem37 7531  ruc 7534  aleph1re 7536  tpsex 7590  0vfval 8210  vsfval 8239  avril1 8769  helloworld 8771  dmadjrnb 9815

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