Theorem mtbir 209

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 204	. 2 |- (-. ph <-> -. ps)
4	1, 3	mpbir 207	1 |- -. ph

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

This theorem is referenced by:  notfal 1265  nonconne 2023  nemtbir 2099  ru 2451  pssirr 2708  npss0 2911  iun0 3309  0iun 3311  vprc 3449  iin0 3477  opprc1b 3542  nlim0 3721  snsn0non 3788  snnex 3801  0nelxp 4066  dm0 4170  iprc 4210  co02 4411  imadif 4493  tz7.44lem1 5135  tz7.44-2 5137  tz7.48-3 5167  canth2 5548  undefnel2 5558  rankpw 5795  zorn 5959  brdom3 5963  cfsuc 6063  0npq 6202  1pr 6269  0nsr 6340  0ncn 6403  ax1ne0 6433  pnfnre 6665  mnfnre 6666  xrltnr 6716  nn0sub 7370  sqr2irr 7979  inelr 7985  climubii 8413  eirr 8656  ruclem35 8813  ruclem37 8815  ruc 8818  aleph1re 8820  tpsex 8874  vsfval 9586  avril1 10142  helloworld 10144  fsubbas 10281  zrdivrng 10418  dmadjrnb 11467  bnj521 12522  1nprm 13769  3prm 13780  3pm3.2ni 13809  indifdi 13823  elpotr 13847  dfon2lem7 13855  poseq 13954  nosgnn0 13999  axsltsolem1 14006  mont 14159  subsym1 14251  inpc 14619  zrfld 14784  top2usne 14898  elfiun 15369  ufilen 15579  compne 16417

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 164

Copyright terms: Public domain