Theorem mtbird 674

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 664	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  2292  neleqtrrd  2295  eqnbrtrd  4051  fidifsnen  6931  php5fin  6943  tridc  6960  fimax2gtrilemstep  6961  en2eqpr  6968  inflbti  7090  omp1eomlem  7160  difinfsnlem  7165  addnidpig  7403  nqnq0pi  7505  ltpopr  7662  cauappcvgprlemladdru  7723  caucvgprlemladdrl  7745  caucvgprprlemnkltj  7756  caucvgprprlemnkeqj  7757  caucvgprprlemaddq  7775  ltposr  7830  axpre-suploclemres  7968  axltirr  8093  reapirr  8604  apirr  8632  indstr2  9683  xrltnsym  9868  xrlttr  9870  xrltso  9871  xltadd1  9951  xposdif  9957  xleaddadd  9962  lbioog  9988  ubioog  9989  fzn  10117  xqltnle  10357  flqltnz  10377  iseqf1olemnab  10593  iseqf1olemqk  10599  exp3val  10633  fihashelne0d  10889  zfz1isolemiso  10931  xrmaxltsup  11423  binomlem  11648  dvdsle  12009  2tp1odd  12049  divalglemeuneg  12088  bits0e  12113  bezoutlemle  12175  rpexp  12321  oddpwdclemxy  12337  oddpwdclemndvds  12339  sqpweven  12343  2sqpwodd  12344  oddprm  12428  pythagtriplem11  12443  pythagtriplem13  12445  pcpremul  12462  pczndvds2  12487  pc2dvds  12499  pcmpt  12512  ctinfom  12645  aprirr  13839  ivthinc  14879  logbgcd1irraplemexp  15204  lgsval2lem  15251  lgsdir  15276  lgsne0  15279  gausslemma2dlem1f1o  15301  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem4  15314  lgsquadlem1  15318  lgsquad2  15324  m1lgs  15326  2sqlem7  15362  neapmkvlem  15711