Theorem pm2.65da 816

Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

Hypotheses

Ref	Expression
pm2.65da.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
pm2.65da.2	⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)

Assertion

Ref	Expression
pm2.65da	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.65da

Step	Hyp	Ref	Expression
1		pm2.65da.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 416	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 210  df-an 400

This theorem is referenced by:  condan  817  nelrdva  3644  onnseq  7964  oeeulem  8210  disjen  8658  cantnflem1  9136  ssfin4  9721  fin1a2lem12  9822  fin1a2lem13  9823  canthnumlem  10059  canthwelem  10061  supaddc  11595  supmul1  11597  ixxdisj  12741  ixxub  12747  ixxlb  12748  icodisj  12854  discr1  13596  sqrlem7  14600  bitsfzolem  15773  bitsfzo  15774  sqnprm  16036  mreexexlem2d  16908  acsinfd  17782  simpgntrivd  19213  prmgrpsimpgd  19229  ablsimpgprmd  19230  lbsextlem3  19925  lbsextlem4  19926  iunconn  22033  dissnlocfin  22134  ptcmplem4  22660  iccntr  23426  evth  23564  bcthlem5  23932  ovolicopnf  24128  vitalilem4  24215  dvferm1  24588  dvferm2  24590  dgreq0  24862  radcnvle  25015  isosctrlem2  25405  dmlogdmgm  25609  mersenne  25811  2sqn0  26018  pntlem3  26193  ostth2lem1  26202  tgbtwnne  26284  tglowdim1i  26295  tgbtwndiff  26300  tgbtwnconn1lem3  26368  legso  26393  tglineintmo  26436  tglineneq  26438  tglowdim2ln  26445  mirne  26461  mirhl  26473  krippenlem  26484  midexlem  26486  footexALT  26512  footexlem2  26514  colperpexlem3  26526  mideulem2  26528  opphllem  26529  oppnid  26540  opphllem2  26542  outpasch  26549  hlpasch  26550  hpgerlem  26559  colhp  26564  trgcopy  26598  tgasa1  26652  umgrnloop2  26939  ex-natded5.5  28195  ex-natded5.8  28198  ex-natded5.13  28200  unidifsnne  30308  nn0min  30562  ornglmullt  30931  orngrmullt  30932  0nellinds  30986  pidlnz  30991  0ringprmidl  31033  qsidomlem1  31036  krull  31051  lvecdim0  31093  lindsunlem  31108  zarcls1  31222  zarclsint  31225  qqhre  31371  esumcvgre  31460  carsgclctunlem2  31687  oddpwdc  31722  eulerpartlemf  31738  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemimin  31873  ballotlem1c  31875  reprinfz1  32003  bnj1417  32423  unbdqndv2lem2  33962  knoppndvlem13  33976  irrdiff  34740  topdifinffinlem  34764  pibt2  34834  poimirlem11  35068  poimirlem12  35069  imo72b2  40878  iunconnlem2  41641  n0p  41677  uzwo4  41687  ssnct  41713  nsstr  41731  disjrnmpt2  41815  difmap  41836  difmapsn  41841  mapssbi  41842  xrlexaddrp  41984  infleinflem2  42003  xrralrecnnge  42026  supminfxr2  42108  xrpnf  42125  icoub  42163  ioonct  42174  ressioosup  42192  ressiooinf  42194  limclner  42293  limsupub  42346  climxrrelem  42391  climlimsupcex  42411  icccncfext  42529  fperdvper  42561  dvdivbd  42565  dvdsn1add  42581  dvmptfprodlem  42586  dvnprodlem3  42590  fourierdlem10  42759  fourierdlem19  42768  fourierdlem20  42769  fourierdlem35  42784  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem57  42805  fourierdlem58  42806  fourierdlem59  42807  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem68  42816  fourierdlem74  42822  fourierdlem75  42823  fourierdlem78  42826  fourierdlem79  42827  fourierdlem80  42828  elaa2  42876  etransclem35  42911  etransclem38  42914  fge0npnf  43006  sge0tsms  43019  sge0rern  43027  sge0supre  43028  sge0le  43046  sge0fodjrnlem  43055  sge0rpcpnf  43060  meadjun  43101  meadjiunlem  43104  hoidmvlelem2  43235  hspdifhsp  43255  ovolval4lem1  43288