Theorem mtand 691

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypotheses

Ref	Expression
mtand.1	|- ( ph -> -. ch )
mtand.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mtand	|- ( ph -> -. ps )

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 |- ( ph -> -. ch )
2		mtand.2	. . 3 |- ( ( ph /\ ps ) -> ch )
3	2	ex 450	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mtod 189	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

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  df-an 386

This theorem is referenced by:  peano5  7089  wfrlem16  7430  sdomnsym  8085  unxpdomlem2  8165  cnfcom2lem  8598  cflim2  9085  fin23lem39  9172  isf32lem2  9176  konigthlem  9390  pythagtriplem4  15524  pythagtriplem11  15530  pythagtriplem13  15532  prmreclem1  15620  psgnunilem5  17914  sylow1lem3  18015  efgredlema  18153  efgredlemc  18158  lssvancl1  18945  lspexchn1  19130  lspindp1  19133  evlslem3  19514  zringlpirlem3  19834  reconnlem2  22630  aaliou2  24095  logdmnrp  24387  dmgmaddnn0  24753  pntpbnd1  25275  ostth2lem4  25325  ncolcom  25456  ncolrot1  25457  ncolrot2  25458  ncoltgdim2  25460  hleqnid  25503  ncolne1  25520  ncolncol  25541  miriso  25565  mirbtwnhl  25575  symquadlem  25584  ragncol  25604  mideulem2  25626  opphllem2  25640  opphllem4  25642  opphl  25646  hpgerlem  25657  lmieu  25676  2sqcoprm  29647  lmdvg  29999  ballotlemfcc  30555  ballotlemi1  30564  ballotlemii  30565  tgoldbachgtda  30739  nosepssdm  31836  nolt02olem  31844  nolt02o  31845  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  nocvxminlem  31893  lindsenlbs  33404  mblfinlem1  33446  lcvnbtwn  34312  ncvr1  34559  lnnat  34713  lplncvrlvol  34902  dalem39  34997  lhpocnle  35302  cdleme17b  35574  cdlemg31c  35987  lclkrlem2o  36810  lcfrlem19  36850  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdh8ab  37066  mapdh8ad  37068  mapdh8c  37070  fphpd  37380  fiphp3d  37383  pellexlem6  37398  elpell1qr2  37436  pellqrex  37443  pellfund14gap  37451  unxpwdom3  37665  dvgrat  38511  nelpr2  39261  nelpr1  39262  limcperiod  39860  sumnnodd  39862  stirlinglem5  40295  dirkercncflem2  40321  fourierdlem25  40349  fourierdlem63  40386  elaa2  40451  etransclem9  40460  etransclem41  40492  etransclem44  40495