Theorem mtbird 679

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  2327  neleqtrrd  2330  eqnbrtrd  4106  fidifsnen  7056  php5fin  7070  tridc  7088  fimax2gtrilemstep  7089  en2eqpr  7098  inflbti  7222  omp1eomlem  7292  difinfsnlem  7297  addnidpig  7555  nqnq0pi  7657  ltpopr  7814  cauappcvgprlemladdru  7875  caucvgprlemladdrl  7897  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemaddq  7927  ltposr  7982  axpre-suploclemres  8120  axltirr  8245  reapirr  8756  apirr  8784  indstr2  9842  xrltnsym  10027  xrlttr  10029  xrltso  10030  xltadd1  10110  xposdif  10116  xleaddadd  10121  lbioog  10147  ubioog  10148  fzn  10276  xqltnle  10526  flqltnz  10546  iseqf1olemnab  10762  iseqf1olemqk  10768  exp3val  10802  fihashelne0d  11058  zfz1isolemiso  11102  swrdnd  11239  swrd0g  11240  xrmaxltsup  11818  binomlem  12043  dvdsle  12404  2tp1odd  12444  divalglemeuneg  12483  bits0e  12509  bezoutlemle  12578  rpexp  12724  oddpwdclemxy  12740  oddpwdclemndvds  12742  sqpweven  12746  2sqpwodd  12747  oddprm  12831  pythagtriplem11  12846  pythagtriplem13  12848  pcpremul  12865  pczndvds2  12890  pc2dvds  12902  pcmpt  12915  ctinfom  13048  aprirr  14296  ivthinc  15366  logbgcd1irraplemexp  15691  lgsval2lem  15738  lgsdir  15763  lgsne0  15766  gausslemma2dlem1f1o  15788  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem4  15801  lgsquadlem1  15805  lgsquad2  15811  m1lgs  15813  2sqlem7  15849  1loopgrvd0fi  16156  neapmkvlem  16671