Theorem mtbid 314

Description: A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

Hypotheses

Ref	Expression
mtbid.min	|- ( ph -> -. ps )
mtbid.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mtbid	|- ( ph -> -. ch )

Proof of Theorem mtbid

Step	Hyp	Ref	Expression
1		mtbid.min	. 2 |- ( ph -> -. ps )
2		mtbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 238	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mtod 189	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  sylnib  318  neleqtrd  2722  eueq3  3381  efrirr  5095  efrn2lp  5096  epne3  6980  wfrlem10  7424  ordtypelem9  8431  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1  8586  cnfcom3lem  8600  cflim2  9085  fin23lem30  9164  isf32lem5  9179  axdc3lem4  9275  axpownd  9423  pwfseqlem3  9482  grur1  9642  genpnnp  9827  xrlttri  11972  expneg  12868  bcval5  13105  seqcoll  13248  seqcoll2  13249  hashge2el2dif  13262  fsumss  14456  fprodss  14678  oddsumodd  15113  rpdvds  15374  pcmpt  15596  prmreclem2  15621  prmreclem5  15624  prmlem0  15812  sylow1lem3  18015  sylow2blem3  18037  efgredlema  18153  gsum2d2lem  18372  lindsind2  20158  1stccnp  21265  kqdisj  21535  alexsubALTlem4  21854  xrhmeo  22745  minveclem3b  23199  ovolgelb  23248  volsup  23324  volsup2  23373  itg1val2  23451  itg2seq  23509  itg2cn  23530  limcnlp  23642  itgsubstlem  23811  ply1termlem  23959  radcnvlt1  24172  fsumharmonic  24738  ftalem3  24801  chpub  24945  lgsqr  25076  lgseisenlem1  25100  lgsquadlem3  25107  2sqlem8a  25150  2sqlem8  25151  2sqblem  25156  tgdim01  25402  lnoppnhpg  25656  acopyeu  25725  axcontlem2  25845  minvecolem5  27737  divnumden2  29564  esum2d  30155  oddpwdc  30416  eulerpartlemsv2  30420  eulerpartlemv  30426  eulerpartlemgh  30440  signslema  30639  erdszelem7  31179  erdszelem8  31180  wsuclem  31773  wsuclemOLD  31774  nosupbnd1lem2  31855  nosupbnd2  31862  knoppndvlem10  32512  knoppndvlem13  32515  lindsdom  33403  ftc1anclem5  33489  cntotbnd  33595  lshpdisj  34274  lcv1  34328  atlatmstc  34606  hlatcon2  34738  4noncolr3  34739  3atlem6  34774  lplnnleat  34828  lplnexllnN  34850  lvolnleat  34869  4atlem11  34895  dalem1  34945  dalemswapyzps  34976  dalemrotps  34977  2llnma1  35073  dalawlem15  35171  4atexlemcnd  35358  ltrnel  35425  cdleme15c  35563  cdleme0nex  35577  cdleme20yOLD  35590  cdleme20m  35611  cdleme43bN  35778  cdleme43dN  35780  cdlemeg46nlpq  35805  cdlemg12  35938  dihmeetcN  36591  dihjatc1  36600  dihjatcclem1  36707  lclkrlem2a  36796  lcfrlem20  36851  mapdh6aN  37024  mapdh8ab  37066  hdmap1l6a  37099  irrapxlem1  37386  elpell14qr2  37426  elpell1qr2  37436  wepwsolem  37612  fnwe2lem2  37621  brneqtrd  39248  oddfl  39489  dstregt0  39493  xrlttri5d  39495  divlt0gt0d  39498  supxrgere  39549  supxrgelem  39553  supxrge  39554  suplesup  39555  nepnfltpnf  39558  nemnftgtmnft  39560  infrpge  39567  absimnre  39707  iccdifprioo  39742  climfveq  39901  climfveqf  39912  stoweidlem34  40251  stirlinglem5  40295  dirker2re  40309  dirkerdenne0  40310  dirkertrigeq  40318  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem54  40377  elaa2lem  40450  etransclem9  40460  sge0cl  40598  sge0repnf  40603  sge0split  40626  sge0gtfsumgt  40660  lighneallem1  41522  lighneallem3  41524  0nodd  41810  2nodd  41812  1neven  41932