Theorem mtbird 677

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 667	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2325  neleqtrrd  2328  eqnbrtrd  4102  fidifsnen  7050  php5fin  7062  tridc  7080  fimax2gtrilemstep  7081  en2eqpr  7090  inflbti  7212  omp1eomlem  7282  difinfsnlem  7287  addnidpig  7544  nqnq0pi  7646  ltpopr  7803  cauappcvgprlemladdru  7864  caucvgprlemladdrl  7886  caucvgprprlemnkltj  7897  caucvgprprlemnkeqj  7898  caucvgprprlemaddq  7916  ltposr  7971  axpre-suploclemres  8109  axltirr  8234  reapirr  8745  apirr  8773  indstr2  9831  xrltnsym  10016  xrlttr  10018  xrltso  10019  xltadd1  10099  xposdif  10105  xleaddadd  10110  lbioog  10136  ubioog  10137  fzn  10265  xqltnle  10515  flqltnz  10535  iseqf1olemnab  10751  iseqf1olemqk  10757  exp3val  10791  fihashelne0d  11047  zfz1isolemiso  11090  swrdnd  11227  swrd0g  11228  xrmaxltsup  11806  binomlem  12031  dvdsle  12392  2tp1odd  12432  divalglemeuneg  12471  bits0e  12497  bezoutlemle  12566  rpexp  12712  oddpwdclemxy  12728  oddpwdclemndvds  12730  sqpweven  12734  2sqpwodd  12735  oddprm  12819  pythagtriplem11  12834  pythagtriplem13  12836  pcpremul  12853  pczndvds2  12878  pc2dvds  12890  pcmpt  12903  ctinfom  13036  aprirr  14284  ivthinc  15354  logbgcd1irraplemexp  15679  lgsval2lem  15726  lgsdir  15751  lgsne0  15754  gausslemma2dlem1f1o  15776  lgseisenlem1  15786  lgseisenlem2  15787  lgseisenlem4  15789  lgsquadlem1  15793  lgsquad2  15799  m1lgs  15801  2sqlem7  15837  neapmkvlem  16581