Theorem mtbir 208

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	notbii 203	. 2 |- (-. ph <-> -. ps)
4	1, 3	mpbir 206	1 |- -. ph

Syntax hints:  -. wn 2   <-> wb 162

This theorem is referenced by:  nemtbir 1934  ru 2284  pssirr 2540  npss0 2735  iun0 3130  0iun 3132  vprc 3264  iin0 3292  opprc1b 3357  nlim0 3536  snsn0non 3599  snnex 3612  0nelxp 3877  dm0 3981  iprc 4021  co02 4222  imadif 4304  tz7.44lem1 4946  tz7.44-2 4948  tz7.48-3 4978  canth2 5359  undefnel2 5369  rankpw 5604  zorn 5755  brdom3 5759  cfsuc 5859  0npq 5998  1pr 6065  0nsr 6136  0ncn 6199  ax1ne0 6229  pnfnre 6461  mnfnre 6462  xrltnr 6512  nn0sub 7165  sqr2irr 7774  inelr 7780  climubii 8208  eirr 8451  ruclem35 8608  ruclem37 8610  ruc 8613  aleph1re 8615  tpsex 8669  vsfval 9381  avril1 9937  helloworld 9939  fsubbas 10073  zrdivrng 10210  dmadjrnb 11259  bnj521 12314  1nprm 13561  3prm 13572  3pm3.2ni 13602  indifdi 13617  elpotr 13638  dfon2lem7 13646  poseq 13746  sltval2 13789  nosgnn0 13791  axsltsolem1 13796  mont 13889  subsym1 13981  inpc 14343  zrfld 14507  top2usne 14618  elfiun 15051  ufilen 15261  compne 16099

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 163

Copyright terms: Public domain