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  2289  neleqtrrd  2292  eqnbrtrd  4048  fidifsnen  6928  php5fin  6940  tridc  6957  fimax2gtrilemstep  6958  en2eqpr  6965  inflbti  7085  omp1eomlem  7155  difinfsnlem  7160  addnidpig  7398  nqnq0pi  7500  ltpopr  7657  cauappcvgprlemladdru  7718  caucvgprlemladdrl  7740  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemaddq  7770  ltposr  7825  axpre-suploclemres  7963  axltirr  8088  reapirr  8598  apirr  8626  indstr2  9677  xrltnsym  9862  xrlttr  9864  xrltso  9865  xltadd1  9945  xposdif  9951  xleaddadd  9956  lbioog  9982  ubioog  9983  fzn  10111  xqltnle  10339  flqltnz  10359  iseqf1olemnab  10575  iseqf1olemqk  10581  exp3val  10615  fihashelne0d  10871  zfz1isolemiso  10913  xrmaxltsup  11404  binomlem  11629  dvdsle  11989  2tp1odd  12028  divalglemeuneg  12067  bezoutlemle  12148  rpexp  12294  oddpwdclemxy  12310  oddpwdclemndvds  12312  sqpweven  12316  2sqpwodd  12317  oddprm  12400  pythagtriplem11  12415  pythagtriplem13  12417  pcpremul  12434  pczndvds2  12459  pc2dvds  12471  pcmpt  12484  ctinfom  12588  aprirr  13782  ivthinc  14822  logbgcd1irraplemexp  15141  lgsval2lem  15167  lgsdir  15192  lgsne0  15195  gausslemma2dlem1f1o  15217  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem4  15230  lgsquadlem1  15234  lgsquad2  15240  m1lgs  15242  2sqlem7  15278  neapmkvlem  15627