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  11823  binomlem  12049  dvdsle  12410  2tp1odd  12450  divalglemeuneg  12489  bits0e  12515  bezoutlemle  12584  rpexp  12730  oddpwdclemxy  12746  oddpwdclemndvds  12748  sqpweven  12752  2sqpwodd  12753  oddprm  12837  pythagtriplem11  12852  pythagtriplem13  12854  pcpremul  12871  pczndvds2  12896  pc2dvds  12908  pcmpt  12921  ctinfom  13054  aprirr  14303  ivthinc  15373  logbgcd1irraplemexp  15698  lgsval2lem  15745  lgsdir  15770  lgsne0  15773  gausslemma2dlem1f1o  15795  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem4  15808  lgsquadlem1  15812  lgsquad2  15818  m1lgs  15820  2sqlem7  15856  1loopgrvd0fi  16163  qdiff  16679  neapmkvlem  16698