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  2283  neleqtrrd  2286  eqnbrtrd  4033  fidifsnen  6884  php5fin  6896  tridc  6913  fimax2gtrilemstep  6914  en2eqpr  6921  inflbti  7037  omp1eomlem  7107  difinfsnlem  7112  addnidpig  7349  nqnq0pi  7451  ltpopr  7608  cauappcvgprlemladdru  7669  caucvgprlemladdrl  7691  caucvgprprlemnkltj  7702  caucvgprprlemnkeqj  7703  caucvgprprlemaddq  7721  ltposr  7776  axpre-suploclemres  7914  axltirr  8038  reapirr  8548  apirr  8576  indstr2  9623  xrltnsym  9807  xrlttr  9809  xrltso  9810  xltadd1  9890  xposdif  9896  xleaddadd  9901  lbioog  9927  ubioog  9928  fzn  10056  flqltnz  10301  iseqf1olemnab  10502  iseqf1olemqk  10508  exp3val  10536  fihashelne0d  10791  zfz1isolemiso  10833  xrmaxltsup  11280  binomlem  11505  dvdsle  11864  2tp1odd  11903  divalglemeuneg  11942  bezoutlemle  12023  rpexp  12167  oddpwdclemxy  12183  oddpwdclemndvds  12185  sqpweven  12189  2sqpwodd  12190  oddprm  12273  pythagtriplem11  12288  pythagtriplem13  12290  pcpremul  12307  pczndvds2  12331  pc2dvds  12343  pcmpt  12355  ctinfom  12443  aprirr  13472  ivthinc  14417  logbgcd1irraplemexp  14682  lgsval2lem  14707  lgsdir  14732  lgsne0  14735  lgseisenlem1  14746  lgseisenlem2  14747  m1lgs  14748  2sqlem7  14764  neapmkvlem  15112