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  4148  fidifsnen  7172  php5fin  7186  tridc  7204  fimax2gtrilemstep  7205  en2eqpr  7214  inflbti  7364  omp1eomlem  7434  difinfsnlem  7439  addnidpig  7703  nqnq0pi  7805  ltpopr  7962  cauappcvgprlemladdru  8023  caucvgprlemladdrl  8045  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemaddq  8075  ltposr  8130  axpre-suploclemres  8268  axltirr  8392  reapirr  8907  apirr  8935  indstr2  10018  xrltnsym  10205  xrlttr  10207  xrltso  10208  xltadd1  10288  xposdif  10294  xleaddadd  10299  lbioog  10325  ubioog  10326  fzn  10456  xqltnle  10712  flqltnz  10735  iseqf1olemnab  10951  iseqf1olemqk  10957  exp3val  10991  fihashelne0d  11250  hashf1lem1  11299  zfz1isolemiso  11305  swrdnd  11445  swrd0g  11446  xrmaxltsup  12040  binomlem  12266  dvdsle  12627  2tp1odd  12667  divalglemeuneg  12706  bits0e  12732  bezoutlemle  12801  rpexp  12948  nnmaxpwlemxy  12964  sqpweven  12971  2sqpwodd  12972  oddprm  13058  pythagtriplem11  13073  pythagtriplem13  13075  pcpremul  13092  pczndvds2  13117  pc2dvds  13129  pcmpt  13142  ballotfilem4  13290  ctinfom  13368  aprirr  14644  ivthinc  15793  logbgcd1irraplemexp  16123  birthdaylem3  16146  lgsval2lem  16227  lgsdir  16252  lgsne0  16255  gausslemma2dlem1f1o  16277  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2  16300  m1lgs  16302  2sqlem7  16338  1loopgrvd0fi  16645  qdiff  17196  neapmkvlem  17215