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

Theorem mtbird 647
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 143 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 637 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 588  ax-in2 589
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eqneltrd  2213  neleqtrrd  2216  fidifsnen  6732  php5fin  6744  tridc  6761  fimax2gtrilemstep  6762  en2eqpr  6769  inflbti  6879  omp1eomlem  6947  difinfsnlem  6952  addnidpig  7112  nqnq0pi  7214  ltpopr  7371  cauappcvgprlemladdru  7432  caucvgprlemladdrl  7454  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemaddq  7484  ltposr  7539  axpre-suploclemres  7677  axltirr  7799  reapirr  8307  apirr  8335  indstr2  9371  xrltnsym  9547  xrlttr  9549  xrltso  9550  xltadd1  9627  xposdif  9633  xleaddadd  9638  lbioog  9664  ubioog  9665  fzn  9790  flqltnz  10028  iseqf1olemnab  10229  iseqf1olemqk  10235  exp3val  10263  zfz1isolemiso  10550  xrmaxltsup  10995  binomlem  11220  dvdsle  11469  2tp1odd  11508  divalglemeuneg  11547  bezoutlemle  11623  rpexp  11758  oddpwdclemxy  11774  oddpwdclemndvds  11776  sqpweven  11780  2sqpwodd  11781  ctinfom  11868  ivthinc  12717
  Copyright terms: Public domain W3C validator