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  8905  apirr  8933  indstr2  10009  xrltnsym  10195  xrlttr  10197  xrltso  10198  xltadd1  10278  xposdif  10284  xleaddadd  10289  lbioog  10315  ubioog  10316  fzn  10446  xqltnle  10702  flqltnz  10722  iseqf1olemnab  10938  iseqf1olemqk  10944  exp3val  10978  fihashelne0d  11236  hashf1lem1  11285  zfz1isolemiso  11291  swrdnd  11431  swrd0g  11432  xrmaxltsup  12024  binomlem  12250  dvdsle  12611  2tp1odd  12651  divalglemeuneg  12690  bits0e  12716  bezoutlemle  12785  rpexp  12931  oddpwdclemxy  12947  oddpwdclemndvds  12949  sqpweven  12953  2sqpwodd  12954  oddprm  13038  pythagtriplem11  13053  pythagtriplem13  13055  pcpremul  13072  pczndvds2  13097  pc2dvds  13109  pcmpt  13122  ballotfilem4  13241  ctinfom  13319  aprirr  14595  ivthinc  15744  logbgcd1irraplemexp  16070  birthdaylem3  16089  lgsval2lem  16129  lgsdir  16154  lgsne0  16157  gausslemma2dlem1f1o  16179  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem4  16192  lgsquadlem1  16196  lgsquad2  16202  m1lgs  16204  2sqlem7  16240  1loopgrvd0fi  16547  qdiff  17098  neapmkvlem  17117