Theorem mtbird 679

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 669	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2327  neleqtrrd  2330  eqnbrtrd  4106  fidifsnen  7057  php5fin  7071  tridc  7089  fimax2gtrilemstep  7090  en2eqpr  7099  inflbti  7223  omp1eomlem  7293  difinfsnlem  7298  addnidpig  7556  nqnq0pi  7658  ltpopr  7815  cauappcvgprlemladdru  7876  caucvgprlemladdrl  7898  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemaddq  7928  ltposr  7983  axpre-suploclemres  8121  axltirr  8246  reapirr  8757  apirr  8785  indstr2  9843  xrltnsym  10028  xrlttr  10030  xrltso  10031  xltadd1  10111  xposdif  10117  xleaddadd  10122  lbioog  10148  ubioog  10149  fzn  10277  xqltnle  10528  flqltnz  10548  iseqf1olemnab  10764  iseqf1olemqk  10770  exp3val  10804  fihashelne0d  11060  zfz1isolemiso  11104  swrdnd  11244  swrd0g  11245  xrmaxltsup  11836  binomlem  12062  dvdsle  12423  2tp1odd  12463  divalglemeuneg  12502  bits0e  12528  bezoutlemle  12597  rpexp  12743  oddpwdclemxy  12759  oddpwdclemndvds  12761  sqpweven  12765  2sqpwodd  12766  oddprm  12850  pythagtriplem11  12865  pythagtriplem13  12867  pcpremul  12884  pczndvds2  12909  pc2dvds  12921  pcmpt  12934  ctinfom  13067  aprirr  14316  ivthinc  15386  logbgcd1irraplemexp  15711  lgsval2lem  15758  lgsdir  15783  lgsne0  15786  gausslemma2dlem1f1o  15808  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem4  15821  lgsquadlem1  15825  lgsquad2  15831  m1lgs  15833  2sqlem7  15869  1loopgrvd0fi  16176  qdiff  16704  neapmkvlem  16723