Theorem mtand 816

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

Hypotheses

Ref	Expression
mtand.1	⊢ (𝜑 → ¬ 𝜒)
mtand.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mtand	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtand.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 198	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mteqand  3024  nelpr2  4598  nelpr1  4599  peano5  7837  cofonr  8603  sdomnsym  9033  domnsymfi  9127  unxpdomlem2  9160  cnfcom2lem  9613  cflim2  10176  fin23lem39  10263  isf32lem2  10267  konigthlem  10482  pythagtriplem4  16781  pythagtriplem11  16787  pythagtriplem13  16789  prmreclem1  16878  smndex2dnrinv  18877  psgnunilem5  19460  sylow1lem3  19566  efgredlema  19706  efgredlemc  19711  rrgnz  20672  lssvancl1  20931  lspexchn1  21120  lspindp1  21123  zringlpirlem3  21454  evlslem3  22068  reconnlem2  24803  aaliou2  26317  logdmnrp  26618  dmgmaddnn0  27004  2sqcoprm  27412  pntpbnd1  27563  ostth2lem4  27613  nosepssdm  27664  nolt02olem  27672  nolt02o  27673  nogt01o  27674  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd1lem6  27691  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd1lem6  27706  nocvxminlem  27760  sltsdisj  27809  eqcuts3  27810  ltslpss  27914  cofcutr  27930  ltmuls2  28177  bdayfinbndlem1  28473  z12bdaylem1  28476  ncolcom  28643  ncolrot1  28644  ncolrot2  28645  ncoltgdim2  28647  hleqnid  28690  ncolne1  28707  ncolncol  28728  miriso  28752  mirbtwnhl  28762  symquadlem  28771  ragncol  28791  mideulem2  28816  oppne3  28825  opphllem1  28829  opphllem2  28830  opphllem4  28832  opphl  28836  hpgerlem  28847  lmieu  28866  cgrancol  28911  fracfld  33384  rhmpreimaprmidl  33526  qsnzr  33530  krullndrng  33556  rsprprmprmidl  33597  esplymhp  33727  0ringirng  33849  constrcon  33934  lmdvg  34113  ballotlemfcc  34654  ballotlemi1  34663  ballotlemii  34664  tgoldbachgtda  34821  prv0  35628  ttcwf2  36723  lindsenlbs  37950  mblfinlem1  37992  lcvnbtwn  39485  ncvr1  39732  lnnat  39887  lplncvrlvol  40076  dalem39  40171  lhpocnle  40476  cdleme17b  40747  cdlemg31c  41159  lclkrlem2o  41981  lcfrlem19  42021  baerlem5amN  42176  baerlem5bmN  42177  baerlem5abmN  42178  mapdh8ab  42237  mapdh8ad  42239  mapdh8c  42241  oexpreposd  42768  mullt0b2d  42943  nelsubginvcld  42955  nelsubgcld  42956  fphpd  43262  fiphp3d  43265  pellexlem6  43280  elpell1qr2  43318  pellqrex  43325  pellfund14gap  43333  unxpwdom3  43541  elnelneqd  44647  elnelneq2d  44648  dvgrat  44757  limcperiod  46076  sumnnodd  46078  stirlinglem5  46524  dirkercncflem2  46550  fourierdlem25  46578  fourierdlem63  46615  elaa2  46680  etransclem9  46689  etransclem41  46721  etransclem44  46724  preimagelt  47145  preimalegt  47146  nelsubc2  49556