Theorem mtbir 167

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 162	. 2 ⊢ (¬ φ ↔ ¬ ψ)
4	1, 3	mpbir 165	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 1   ↔ wb 127

This theorem is referenced by:  ru 1437  nvelv 1483  pssirr 1570  opprc1b 1906  opthwiener 1914  snsn0non 2371  opthprc 2457  0nelxp 2475  dmsn0 2543  dmsnsn0 2544  co02 2663  imadif 2714  tz7.44lem1 2965  tz7.44-2 2967  tz7.48-3 2996  0ne1oOLD 3113  map0 3268  canth2 3381  limenpsi 3400  rankpw 3528  zorn2 3612  cfsuc 3709  1pi 3805  0npq 3844  1pr 3911  0nsr 3982  0ncn 4045  ax1ne0 4075  divval 4217  nnunb 4520  avril1 4523  inelr 4527  halfnz 4586  nn0subt 4587  sqr2irr 4782  ruclem37 4921  ruc 4924

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org