Theorem mtbird 675

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 665	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  2301  neleqtrrd  2304  eqnbrtrd  4062  fidifsnen  6967  php5fin  6979  tridc  6996  fimax2gtrilemstep  6997  en2eqpr  7004  inflbti  7126  omp1eomlem  7196  difinfsnlem  7201  addnidpig  7449  nqnq0pi  7551  ltpopr  7708  cauappcvgprlemladdru  7769  caucvgprlemladdrl  7791  caucvgprprlemnkltj  7802  caucvgprprlemnkeqj  7803  caucvgprprlemaddq  7821  ltposr  7876  axpre-suploclemres  8014  axltirr  8139  reapirr  8650  apirr  8678  indstr2  9730  xrltnsym  9915  xrlttr  9917  xrltso  9918  xltadd1  9998  xposdif  10004  xleaddadd  10009  lbioog  10035  ubioog  10036  fzn  10164  xqltnle  10410  flqltnz  10430  iseqf1olemnab  10646  iseqf1olemqk  10652  exp3val  10686  fihashelne0d  10942  zfz1isolemiso  10984  swrdnd  11112  swrd0g  11113  xrmaxltsup  11569  binomlem  11794  dvdsle  12155  2tp1odd  12195  divalglemeuneg  12234  bits0e  12260  bezoutlemle  12329  rpexp  12475  oddpwdclemxy  12491  oddpwdclemndvds  12493  sqpweven  12497  2sqpwodd  12498  oddprm  12582  pythagtriplem11  12597  pythagtriplem13  12599  pcpremul  12616  pczndvds2  12641  pc2dvds  12653  pcmpt  12666  ctinfom  12799  aprirr  14045  ivthinc  15115  logbgcd1irraplemexp  15440  lgsval2lem  15487  lgsdir  15512  lgsne0  15515  gausslemma2dlem1f1o  15537  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem4  15550  lgsquadlem1  15554  lgsquad2  15560  m1lgs  15562  2sqlem7  15598  neapmkvlem  16006