Theorem mtbird 675

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 665	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 615  ax-in2 616

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2302  neleqtrrd  2305  eqnbrtrd  4072  fidifsnen  6988  php5fin  7000  tridc  7017  fimax2gtrilemstep  7018  en2eqpr  7025  inflbti  7147  omp1eomlem  7217  difinfsnlem  7222  addnidpig  7479  nqnq0pi  7581  ltpopr  7738  cauappcvgprlemladdru  7799  caucvgprlemladdrl  7821  caucvgprprlemnkltj  7832  caucvgprprlemnkeqj  7833  caucvgprprlemaddq  7851  ltposr  7906  axpre-suploclemres  8044  axltirr  8169  reapirr  8680  apirr  8708  indstr2  9760  xrltnsym  9945  xrlttr  9947  xrltso  9948  xltadd1  10028  xposdif  10034  xleaddadd  10039  lbioog  10065  ubioog  10066  fzn  10194  xqltnle  10442  flqltnz  10462  iseqf1olemnab  10678  iseqf1olemqk  10684  exp3val  10718  fihashelne0d  10974  zfz1isolemiso  11016  swrdnd  11145  swrd0g  11146  xrmaxltsup  11654  binomlem  11879  dvdsle  12240  2tp1odd  12280  divalglemeuneg  12319  bits0e  12345  bezoutlemle  12414  rpexp  12560  oddpwdclemxy  12576  oddpwdclemndvds  12578  sqpweven  12582  2sqpwodd  12583  oddprm  12667  pythagtriplem11  12682  pythagtriplem13  12684  pcpremul  12701  pczndvds2  12726  pc2dvds  12738  pcmpt  12751  ctinfom  12884  aprirr  14130  ivthinc  15200  logbgcd1irraplemexp  15525  lgsval2lem  15572  lgsdir  15597  lgsne0  15600  gausslemma2dlem1f1o  15622  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem4  15635  lgsquadlem1  15639  lgsquad2  15645  m1lgs  15647  2sqlem7  15683  neapmkvlem  16178