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  4019  fidifsnen  6865  php5fin  6877  tridc  6894  fimax2gtrilemstep  6895  en2eqpr  6902  inflbti  7018  omp1eomlem  7088  difinfsnlem  7093  addnidpig  7330  nqnq0pi  7432  ltpopr  7589  cauappcvgprlemladdru  7650  caucvgprlemladdrl  7672  caucvgprprlemnkltj  7683  caucvgprprlemnkeqj  7684  caucvgprprlemaddq  7702  ltposr  7757  axpre-suploclemres  7895  axltirr  8018  reapirr  8528  apirr  8556  indstr2  9603  xrltnsym  9787  xrlttr  9789  xrltso  9790  xltadd1  9870  xposdif  9876  xleaddadd  9881  lbioog  9907  ubioog  9908  fzn  10035  flqltnz  10280  iseqf1olemnab  10481  iseqf1olemqk  10487  exp3val  10515  fihashelne0d  10768  zfz1isolemiso  10810  xrmaxltsup  11257  binomlem  11482  dvdsle  11840  2tp1odd  11879  divalglemeuneg  11918  bezoutlemle  11999  rpexp  12143  oddpwdclemxy  12159  oddpwdclemndvds  12161  sqpweven  12165  2sqpwodd  12166  oddprm  12249  pythagtriplem11  12264  pythagtriplem13  12266  pcpremul  12283  pczndvds2  12307  pc2dvds  12319  pcmpt  12331  ctinfom  12419  aprirr  13240  ivthinc  13903  logbgcd1irraplemexp  14168  lgsval2lem  14193  lgsdir  14218  lgsne0  14221  2sqlem7  14239  neapmkvlem  14585