Theorem mtand 815

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  3023  nelpr2  4629  nelpr1  4630  peano5  7887  wfrlem16OLD  8336  cofonr  8684  sdomnsym  9110  domnsymfi  9212  unxpdomlem2  9257  cnfcom2lem  9713  cflim2  10275  fin23lem39  10362  isf32lem2  10366  konigthlem  10580  pythagtriplem4  16837  pythagtriplem11  16843  pythagtriplem13  16845  prmreclem1  16934  smndex2dnrinv  18891  psgnunilem5  19473  sylow1lem3  19579  efgredlema  19719  efgredlemc  19724  rrgnz  20662  lssvancl1  20900  lspexchn1  21089  lspindp1  21092  zringlpirlem3  21423  evlslem3  22036  reconnlem2  24765  aaliou2  26298  logdmnrp  26600  dmgmaddnn0  26987  2sqcoprm  27396  pntpbnd1  27547  ostth2lem4  27597  nosepssdm  27648  nolt02olem  27656  nolt02o  27657  nogt01o  27658  nosupbnd1lem3  27672  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  noinfbnd1lem3  27687  noinfbnd1lem4  27688  noinfbnd1lem5  27689  noinfbnd1lem6  27690  nocvxminlem  27739  ssltdisj  27783  sltlpss  27862  cofcutr  27875  sltmul2  28114  ncolcom  28486  ncolrot1  28487  ncolrot2  28488  ncoltgdim2  28490  hleqnid  28533  ncolne1  28550  ncolncol  28571  miriso  28595  mirbtwnhl  28605  symquadlem  28614  ragncol  28634  mideulem2  28659  oppne3  28668  opphllem1  28672  opphllem2  28673  opphllem4  28675  opphl  28679  hpgerlem  28690  lmieu  28709  cgrancol  28754  fracfld  33248  rhmpreimaprmidl  33412  qsnzr  33416  krullndrng  33442  rsprprmprmidl  33483  0ringirng  33676  constrcon  33754  lmdvg  33930  ballotlemfcc  34472  ballotlemi1  34481  ballotlemii  34482  tgoldbachgtda  34639  prv0  35398  lindsenlbs  37585  mblfinlem1  37627  lcvnbtwn  38989  ncvr1  39236  lnnat  39392  lplncvrlvol  39581  dalem39  39676  lhpocnle  39981  cdleme17b  40252  cdlemg31c  40664  lclkrlem2o  41486  lcfrlem19  41526  baerlem5amN  41681  baerlem5bmN  41682  baerlem5abmN  41683  mapdh8ab  41742  mapdh8ad  41744  mapdh8c  41746  oexpreposd  42318  nelsubginvcld  42466  nelsubgcld  42467  fphpd  42786  fiphp3d  42789  pellexlem6  42804  elpell1qr2  42842  pellqrex  42849  pellfund14gap  42857  unxpwdom3  43066  elnelneqd  44173  elnelneq2d  44174  dvgrat  44284  limcperiod  45605  sumnnodd  45607  stirlinglem5  46055  dirkercncflem2  46081  fourierdlem25  46109  fourierdlem63  46146  elaa2  46211  etransclem9  46220  etransclem41  46252  etransclem44  46255  preimagelt  46676  preimalegt  46677  nelsubc2  48984