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

Theorem mtbird 633
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 624 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 579  ax-in2 580
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eqneltrd  2183  neleqtrrd  2186  fidifsnen  6586  php5fin  6598  tridc  6615  fimax2gtrilemstep  6616  en2eqpr  6623  inflbti  6719  addnidpig  6895  nqnq0pi  6997  ltpopr  7154  cauappcvgprlemladdru  7215  caucvgprlemladdrl  7237  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemaddq  7267  ltposr  7309  axltirr  7553  reapirr  8054  apirr  8082  indstr2  9096  xrltnsym  9263  xrlttr  9265  xrltso  9266  lbioog  9331  ubioog  9332  fzn  9456  flqltnz  9694  iseqf1olemnab  9917  iseqf1olemqk  9923  exp3val  9957  zfz1isolemiso  10244  binomlem  10877  dvdsle  11123  2tp1odd  11162  divalglemeuneg  11201  bezoutlemle  11275  rpexp  11410  oddpwdclemxy  11425  oddpwdclemndvds  11427  sqpweven  11431  2sqpwodd  11432
  Copyright terms: Public domain W3C validator