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 4484  rankpw 4684  zorn 4797  brdom3 4801  cfsuc 4915  0npq 5050  1pr 5117  0nsr 5188  0ncn 5251  ax1ne0 5280  pnfnre 5496  mnfnre 5497  xrltnrt 5541  nn0subt 6161  sqr2irr 6729  inelr 6735  climubi 7153  eirr 7394  ruclem35 7544  ruclem37 7546  ruc 7549  aleph1re 7551  tpsex 7605  0vfval 8225  vsfval 8254  avril1 8784  helloworld 8786  dmadjrnb 9830  top2usne 10549

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