Theorem mtbird 673

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 663	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 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eqneltrd  2273  neleqtrrd  2276  eqnbrtrd  4022  fidifsnen  6870  php5fin  6882  tridc  6899  fimax2gtrilemstep  6900  en2eqpr  6907  inflbti  7023  omp1eomlem  7093  difinfsnlem  7098  addnidpig  7335  nqnq0pi  7437  ltpopr  7594  cauappcvgprlemladdru  7655  caucvgprlemladdrl  7677  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemaddq  7707  ltposr  7762  axpre-suploclemres  7900  axltirr  8024  reapirr  8534  apirr  8562  indstr2  9609  xrltnsym  9793  xrlttr  9795  xrltso  9796  xltadd1  9876  xposdif  9882  xleaddadd  9887  lbioog  9913  ubioog  9914  fzn  10042  flqltnz  10287  iseqf1olemnab  10488  iseqf1olemqk  10494  exp3val  10522  fihashelne0d  10777  zfz1isolemiso  10819  xrmaxltsup  11266  binomlem  11491  dvdsle  11850  2tp1odd  11889  divalglemeuneg  11928  bezoutlemle  12009  rpexp  12153  oddpwdclemxy  12169  oddpwdclemndvds  12171  sqpweven  12175  2sqpwodd  12176  oddprm  12259  pythagtriplem11  12274  pythagtriplem13  12276  pcpremul  12293  pczndvds2  12317  pc2dvds  12329  pcmpt  12341  ctinfom  12429  aprirr  13373  ivthinc  14124  logbgcd1irraplemexp  14389  lgsval2lem  14414  lgsdir  14439  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem7  14471  neapmkvlem  14817