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 1633  ru 1928  pssirr 2136  nvelv 2703  iin0 2730  opprc1b 2786  0nelxp 3230  dmsn0 3313  dmsnsn0 3314  inelv 3346  co02 3494  imadif 3560  tz7.44lem1 3912  tz7.44-2 3914  tz7.48-3 3943  canth2 4464  rankpw 4656  zorn 4769  brdom3 4773  cfsuc 4887  0npq 5022  1pr 5089  0nsr 5160  0ncn 5223  ax1ne0 5252  pnfnre 5468  mnfnre 5469  xrltnrt 5514  nn0subt 6108  sqr2irr 6659  inelr 6665  climubi 7089  eirr 7335  ruclem35 7487  ruclem37 7489  ruc 7492  aleph1re 7494  tpsex 7547  0vfval 8163  vsfval 8194  avril1 8723  helloworld 8725  dmadjrnb 9747

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