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

Theorem mtbird 631
Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)
Hypotheses
Ref Expression
mtbird.min  |-  ( ph  ->  -.  ch )
mtbird.maj  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
mtbird  |-  ( ph  ->  -.  ps )

Proof of Theorem mtbird
StepHypRef Expression
1 mtbird.min . 2  |-  ( ph  ->  -.  ch )
2 mtbird.maj . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
32biimpd 142 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 622 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eqneltrd  2175  neleqtrrd  2178  fidifsnen  6405  php5fin  6416  en2eqpr  6434  inflbti  6496  addnidpig  6588  nqnq0pi  6690  ltpopr  6847  cauappcvgprlemladdru  6908  caucvgprlemladdrl  6930  caucvgprprlemnkltj  6941  caucvgprprlemnkeqj  6942  caucvgprprlemaddq  6960  ltposr  7002  axltirr  7246  reapirr  7744  apirr  7772  indstr2  8777  xrltnsym  8944  xrlttr  8946  xrltso  8947  lbioog  9012  ubioog  9013  fzn  9137  flqltnz  9369  expival  9575  dvdsle  10389  2tp1odd  10428  divalglemeuneg  10467  bezoutlemle  10541  rpexp  10676  oddpwdclemxy  10691  oddpwdclemndvds  10693  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator