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  11540  binomlem  11765  dvdsle  12126  2tp1odd  12166  divalglemeuneg  12205  bits0e  12231  bezoutlemle  12300  rpexp  12446  oddpwdclemxy  12462  oddpwdclemndvds  12464  sqpweven  12468  2sqpwodd  12469  oddprm  12553  pythagtriplem11  12568  pythagtriplem13  12570  pcpremul  12587  pczndvds2  12612  pc2dvds  12624  pcmpt  12637  ctinfom  12770  aprirr  14016  ivthinc  15086  logbgcd1irraplemexp  15411  lgsval2lem  15458  lgsdir  15483  lgsne0  15486  gausslemma2dlem1f1o  15508  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem4  15521  lgsquadlem1  15525  lgsquad2  15531  m1lgs  15533  2sqlem7  15569  neapmkvlem  15968