Theorem mtbird 680

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 669	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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2328  neleqtrrd  2331  eqnbrtrd  4127  fidifsnen  7125  php5fin  7139  tridc  7157  fimax2gtrilemstep  7158  en2eqpr  7167  inflbti  7315  omp1eomlem  7385  difinfsnlem  7390  addnidpig  7651  nqnq0pi  7753  ltpopr  7910  cauappcvgprlemladdru  7971  caucvgprlemladdrl  7993  caucvgprprlemnkltj  8004  caucvgprprlemnkeqj  8005  caucvgprprlemaddq  8023  ltposr  8078  axpre-suploclemres  8216  axltirr  8340  reapirr  8851  apirr  8879  indstr2  9941  xrltnsym  10126  xrlttr  10128  xrltso  10129  xltadd1  10209  xposdif  10215  xleaddadd  10220  lbioog  10246  ubioog  10247  fzn  10376  xqltnle  10627  flqltnz  10647  iseqf1olemnab  10863  iseqf1olemqk  10869  exp3val  10903  fihashelne0d  11160  zfz1isolemiso  11211  swrdnd  11351  swrd0g  11352  xrmaxltsup  11943  binomlem  12169  dvdsle  12530  2tp1odd  12570  divalglemeuneg  12609  bits0e  12635  bezoutlemle  12704  rpexp  12850  oddpwdclemxy  12866  oddpwdclemndvds  12868  sqpweven  12872  2sqpwodd  12873  oddprm  12957  pythagtriplem11  12972  pythagtriplem13  12974  pcpremul  12991  pczndvds2  13016  pc2dvds  13028  pcmpt  13041  ctinfom  13179  aprirr  14429  ivthinc  15508  logbgcd1irraplemexp  15833  lgsval2lem  15883  lgsdir  15908  lgsne0  15911  gausslemma2dlem1f1o  15933  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem4  15946  lgsquadlem1  15950  lgsquad2  15956  m1lgs  15958  2sqlem7  15994  1loopgrvd0fi  16301  qdiff  16833  neapmkvlem  16853