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 1644  ru 1941  pssirr 2149  nvelv 2718  iin0 2745  opprc1b 2802  0nelxp 3246  dmsn0 3330  dmsnsn0 3331  inelv 3368  co02 3514  imadif 3580  tz7.44lem1 3933  tz7.44-2 3935  tz7.48-3 3964  canth2 4490  rankpw 4694  zorn 4807  brdom3 4811  cfsuc 4927  0npq 5062  1pr 5129  0nsr 5200  0ncn 5263  ax1ne0 5292  pnfnre 5508  mnfnre 5509  xrltnrt 5553  nn0subt 6163  sqr2irr 6730  inelr 6736  climubi 7153  eirr 7394  ruclem35 7545  ruclem37 7547  ruc 7550  aleph1re 7552  tpsex 7606  0vfval 8221  vsfval 8250  avril1 8779  helloworld 8781  dmadjrnb 9825  inpc 10476  top2usne 10535

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