ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtbir Unicode version

Theorem mtbir 672
Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.)
Hypotheses
Ref Expression
mtbir.1  |-  -.  ps
mtbir.2  |-  ( ph  <->  ps )
Assertion
Ref Expression
mtbir  |-  -.  ph

Proof of Theorem mtbir
StepHypRef Expression
1 mtbir.1 . 2  |-  -.  ps
2 mtbir.2 . . 3  |-  ( ph  <->  ps )
32bicomi 132 . 2  |-  ( ps  <->  ph )
41, 3mtbi 671 1  |-  -.  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  nnexmid  851  nndc  852  fal  1371  ax-9  1542  nonconne  2372  nemtbir  2449  ru  2976  noel  3441  iun0  3958  0iun  3959  br0  4066  vprc  4150  iin0r  4187  nlim0  4412  snnex  4466  onsucelsucexmid  4547  0nelxp  4672  dm0  4859  iprc  4913  co02  5160  0fv  5570  frec0g  6422  nnsucuniel  6520  1nen2  6889  fidcenumlemrk  6983  djulclb  7084  ismkvnex  7183  pw1ne3  7259  sucpw1nel3  7262  3nsssucpw1  7265  0nnq  7393  0npr  7512  nqprdisj  7573  0ncn  7860  axpre-ltirr  7911  pnfnre  8029  mnfnre  8030  inelr  8571  xrltnr  9809  fzo0  10198  fzouzdisj  10210  inftonninf  10472  hashinfom  10790  3prm  12160  sqrt2irr  12194  ennnfonelem1  12458  bj-nndcALT  14971  bj-vprc  15109  pwle2  15210  exmidsbthrlem  15232
  Copyright terms: Public domain W3C validator