Theorem mtbir 192

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

Hypotheses

Ref	Expression
mtbir.1	⊢ ¬ ψ
mtbir.2	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mtbir	⊢ ¬ φ

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 ⊢ ¬ ψ
2		mtbir.2	. . 3 ⊢ (φ ↔ ψ)
3	2	negbii 187	. 2 ⊢ (¬ φ ↔ ¬ ψ)
4	1, 3	mpbir 190	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 2   ↔ wb 146

This theorem is referenced by:  nemtbir 1638  ru 1934  pssirr 2142  nvelv 2708  iin0 2735  opprc1b 2791  0nelxp 3235  dmsn0 3319  dmsnsn0 3320  inelv 3354  co02 3500  imadif 3566  tz7.44lem1 3918  tz7.44-2 3920  tz7.48-3 3949  canth2 4470  rankpw 4664  zorn 4777  brdom3 4781  cfsuc 4895  0npq 5030  1pr 5097  0nsr 5168  0ncn 5231  ax1ne0 5260  pnfnre 5476  mnfnre 5477  xrltnrt 5522  nn0subt 6116  sqr2irr 6667  inelr 6673  climubi 7097  eirr 7343  ruclem35 7495  ruclem37 7497  ruc 7500  aleph1re 7502  tpsex 7555  0vfval 8177  vsfval 8206  avril1 8723  helloworld 8725  dmadjrnb 9770

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