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  2300  neleqtrrd  2303  eqnbrtrd  4061  fidifsnen  6966  php5fin  6978  tridc  6995  fimax2gtrilemstep  6996  en2eqpr  7003  inflbti  7125  omp1eomlem  7195  difinfsnlem  7200  addnidpig  7448  nqnq0pi  7550  ltpopr  7707  cauappcvgprlemladdru  7768  caucvgprlemladdrl  7790  caucvgprprlemnkltj  7801  caucvgprprlemnkeqj  7802  caucvgprprlemaddq  7820  ltposr  7875  axpre-suploclemres  8013  axltirr  8138  reapirr  8649  apirr  8677  indstr2  9729  xrltnsym  9914  xrlttr  9916  xrltso  9917  xltadd1  9997  xposdif  10003  xleaddadd  10008  lbioog  10034  ubioog  10035  fzn  10163  xqltnle  10408  flqltnz  10428  iseqf1olemnab  10644  iseqf1olemqk  10650  exp3val  10684  fihashelne0d  10940  zfz1isolemiso  10982  xrmaxltsup  11511  binomlem  11736  dvdsle  12097  2tp1odd  12137  divalglemeuneg  12176  bits0e  12202  bezoutlemle  12271  rpexp  12417  oddpwdclemxy  12433  oddpwdclemndvds  12435  sqpweven  12439  2sqpwodd  12440  oddprm  12524  pythagtriplem11  12539  pythagtriplem13  12541  pcpremul  12558  pczndvds2  12583  pc2dvds  12595  pcmpt  12608  ctinfom  12741  aprirr  13987  ivthinc  15057  logbgcd1irraplemexp  15382  lgsval2lem  15429  lgsdir  15454  lgsne0  15457  gausslemma2dlem1f1o  15479  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem4  15492  lgsquadlem1  15496  lgsquad2  15502  m1lgs  15504  2sqlem7  15540  neapmkvlem  15939