Theorem mtbird 684

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

Step	Hyp	Ref	Expression
1		mtbird.min	. 2 |- ( ph -> -. ch )
2		mtbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 673	1 |- ( ph -> -. ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117

This theorem is used by:  eqneltrd  2334  neleqtrrd  2337  eqnbrtrd  4149  fidifsnen  7178  php5fin  7192  tridc  7210  fimax2gtrilemstep  7211  en2eqpr  7220  inflbti  7370  omp1eomlem  7440  difinfsnlem  7445  addnidpig  7709  nqnq0pi  7811  ltpopr  7968  cauappcvgprlemladdru  8029  caucvgprlemladdrl  8051  caucvgprprlemnkltj  8062  caucvgprprlemnkeqj  8063  caucvgprprlemaddq  8081  ltposr  8136  axpre-suploclemres  8274  axltirr  8398  reapirr  8913  apirr  8941  indstr2  10024  xrltnsym  10211  xrlttr  10213  xrltso  10214  xltadd1  10294  xposdif  10300  xleaddadd  10305  lbioog  10331  ubioog  10332  fzn  10462  xqltnle  10718  flqltnz  10742  iseqf1olemnab  10958  iseqf1olemqk  10964  exp3val  10998  fihashelne0d  11257  hashf1lem1  11306  zfz1isolemiso  11312  swrdnd  11452  swrd0g  11453  xrmaxltsup  12048  binomlem  12274  dvdsle  12635  2tp1odd  12675  divalglemeuneg  12714  bits0e  12740  bezoutlemle  12809  rpexp  12956  nnmaxpwlemxy  12972  sqpweven  12979  2sqpwodd  12980  oddprm  13066  pythagtriplem11  13081  pythagtriplem13  13083  pcpremul  13100  pczndvds2  13125  pc2dvds  13137  pcmpt  13150  ballotfilem4  13298  ctinfom  13376  aprirr  14703  ivthinc  15886  logbgcd1irraplemexp  16221  birthdaylem3  16244  chtqub  16313  lgsval2lem  16351  lgsdir  16376  lgsne0  16379  gausslemma2dlem1f1o  16401  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem4  16414  lgsquadlem1  16418  lgsquad2  16424  m1lgs  16426  2sqlem7  16462  1loopgrvd0fi  16769  rirrdisj  17308  qdiff  17322  neapmkvlem  17341