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 412	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 412	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 196	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:  condan  817  nelrdva  3688  eqsnuniex  5331  onnseq  8356  oeeulem  8611  disjen  9146  cantnflem1  9701  ssfin4  10322  fin1a2lem12  10423  fin1a2lem13  10424  canthnumlem  10660  canthwelem  10662  supaddc  12207  supmul1  12209  ixxdisj  13375  ixxub  13381  ixxlb  13382  icodisj  13491  discr1  14255  01sqrexlem7  15265  bitsfzolem  16451  bitsfzo  16452  sqnprm  16719  mreexexlem2d  17655  acsinfd  18564  simpgntrivd  20079  prmgrpsimpgd  20095  ablsimpgprmd  20096  lbsextlem3  21119  lbsextlem4  21120  iunconn  23364  dissnlocfin  23465  ptcmplem4  23991  iccntr  24759  evth  24907  bcthlem5  25278  ovolicopnf  25475  vitalilem4  25562  dvferm1  25939  dvferm2  25941  dgreq0  26221  radcnvle  26379  isosctrlem2  26779  dmlogdmgm  26984  mersenne  27188  2sqn0  27395  pntlem3  27570  ostth2lem1  27579  tgbtwnne  28415  tglowdim1i  28426  tgbtwndiff  28431  tgbtwnconn1lem3  28499  legso  28524  tglineintmo  28567  tglineneq  28569  tglowdim2ln  28576  mirne  28592  mirhl  28604  krippenlem  28615  midexlem  28617  footexALT  28643  footexlem2  28645  colperpexlem3  28657  mideulem2  28659  opphllem  28660  oppnid  28671  opphllem2  28673  outpasch  28680  hlpasch  28681  hpgerlem  28690  colhp  28695  trgcopy  28729  tgasa1  28783  umgrnloop2  29071  ex-natded5.5  30337  ex-natded5.8  30340  ex-natded5.13  30342  unidifsnne  32463  ifnefals  32475  rexmul2  32677  hashpss  32734  nn0min  32745  ccatws1f1o  32873  elrgspnlem2  33184  fracfld  33248  ornglmullt  33275  orngrmullt  33276  0nellinds  33331  pidlnz  33337  drngidl  33394  drngidlhash  33395  0ringprmidl  33410  qsidomlem1  33413  mxidlirredi  33432  krull  33440  qsdrngi  33456  qsdrng  33458  rsprprmprmidlb  33484  rprmasso2  33487  1arithidom  33498  pidufd  33504  1arithufdlem3  33507  dfufd2  33511  0ringmon1p  33516  ig1pnunit  33556  exsslsb  33582  lvecdim0  33592  lindsunlem  33610  assafld  33623  fldextrspundgdvdslem  33667  irredminply  33696  constrextdg2lem  33728  constrext2chnlem  33730  2sqr3nconstr  33761  zarcls1  33846  zarclsint  33849  qqhre  33997  esumcvgre  34068  carsgclctunlem2  34297  oddpwdc  34332  eulerpartlemf  34348  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemimin  34484  ballotlem1c  34486  reprinfz1  34600  bnj1417  35018  unbdqndv2lem2  36474  knoppndvlem13  36488  irrdiff  37290  topdifinffinlem  37311  pibt2  37381  poimirlem11  37601  poimirlem12  37602  aks4d1p7  42042  aks4d1p8d2  42044  aks4d1p8  42046  aks4d1p9  42047  fldhmf1  42049  hashscontpow1  42080  aks6d1c5  42098  imo72b2  44143  iunconnlem2  44907  n0p  45017  uzwo4  45025  ssnct  45049  nsstr  45067  disjrnmpt2  45160  difmap  45179  difmapsn  45184  mapssbi  45185  xrlexaddrp  45327  infleinflem2  45346  xrralrecnnge  45365  supminfxr2  45444  xrpnf  45460  icoub  45503  ioonct  45514  ressioosup  45532  ressiooinf  45534  limclner  45628  limsupub  45681  climxrrelem  45726  climlimsupcex  45746  icccncfext  45864  fperdvper  45896  dvdivbd  45900  dvdsn1add  45916  dvmptfprodlem  45921  dvnprodlem3  45925  fourierdlem10  46094  fourierdlem19  46103  fourierdlem20  46104  fourierdlem35  46119  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem68  46151  fourierdlem74  46157  fourierdlem75  46158  fourierdlem78  46161  fourierdlem79  46162  fourierdlem80  46163  elaa2  46211  etransclem35  46246  etransclem38  46249  fge0npnf  46344  sge0tsms  46357  sge0rern  46365  sge0supre  46366  sge0le  46384  sge0fodjrnlem  46393  sge0rpcpnf  46398  meadjun  46439  meadjiunlem  46442  hoidmvlelem2  46573  hspdifhsp  46593  ovolval4lem1  46626