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 1617  ru 1909  pssirr 2117  nvelv 2681  iin0 2708  opprc1b 2763  0nelxp 3202  dmsn0 3281  dmsnsn0 3282  inelv 3290  co02 3450  imadif 3514  tz7.44lem1 3866  tz7.44-2 3868  tz7.48-3 3897  canth2 4418  rankpw 4608  zorn 4721  brdom3 4725  cfsuc 4838  0npq 4973  1pr 5040  0nsr 5111  0ncn 5174  ax1ne0 5203  xrltnrt 5465  nn0subt 6059  sqr2irr 6610  inelr 6616  climubi 7040  eirr 7286  ruclem35 7438  ruclem37 7440  ruc 7443  aleph1re 7445  tpsex 7498  0vfval 8105  vsfval 8132  avril1 8964  helloworld 8966  dmadjrnb 9961

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