Theorem pm2.65da 813

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 195	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 206  df-an 396

This theorem is referenced by:  condan  814  nelrdva  3635  eqsnuniex  5278  onnseq  8146  oeeulem  8394  disjen  8870  cantnflem1  9377  ssfin4  9997  fin1a2lem12  10098  fin1a2lem13  10099  canthnumlem  10335  canthwelem  10337  supaddc  11872  supmul1  11874  ixxdisj  13023  ixxub  13029  ixxlb  13030  icodisj  13137  discr1  13882  sqrlem7  14888  bitsfzolem  16069  bitsfzo  16070  sqnprm  16335  mreexexlem2d  17271  acsinfd  18189  simpgntrivd  19616  prmgrpsimpgd  19632  ablsimpgprmd  19633  lbsextlem3  20337  lbsextlem4  20338  iunconn  22487  dissnlocfin  22588  ptcmplem4  23114  iccntr  23890  evth  24028  bcthlem5  24397  ovolicopnf  24593  vitalilem4  24680  dvferm1  25054  dvferm2  25056  dgreq0  25331  radcnvle  25484  isosctrlem2  25874  dmlogdmgm  26078  mersenne  26280  2sqn0  26487  pntlem3  26662  ostth2lem1  26671  tgbtwnne  26755  tglowdim1i  26766  tgbtwndiff  26771  tgbtwnconn1lem3  26839  legso  26864  tglineintmo  26907  tglineneq  26909  tglowdim2ln  26916  mirne  26932  mirhl  26944  krippenlem  26955  midexlem  26957  footexALT  26983  footexlem2  26985  colperpexlem3  26997  mideulem2  26999  opphllem  27000  oppnid  27011  opphllem2  27013  outpasch  27020  hlpasch  27021  hpgerlem  27030  colhp  27035  trgcopy  27069  tgasa1  27123  umgrnloop2  27419  ex-natded5.5  28675  ex-natded5.8  28678  ex-natded5.13  28680  unidifsnne  30785  nn0min  31036  ornglmullt  31408  orngrmullt  31409  0nellinds  31468  pidlnz  31473  0ringprmidl  31527  qsidomlem1  31530  krull  31545  lvecdim0  31592  lindsunlem  31607  zarcls1  31721  zarclsint  31724  qqhre  31870  esumcvgre  31959  carsgclctunlem2  32186  oddpwdc  32221  eulerpartlemf  32237  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemimin  32372  ballotlem1c  32374  reprinfz1  32502  bnj1417  32921  unbdqndv2lem2  34617  knoppndvlem13  34631  irrdiff  35424  topdifinffinlem  35445  pibt2  35515  poimirlem11  35715  poimirlem12  35716  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8  40023  aks4d1p9  40024  imo72b2  41672  iunconnlem2  42444  n0p  42480  uzwo4  42490  ssnct  42516  nsstr  42534  disjrnmpt2  42615  difmap  42636  difmapsn  42641  mapssbi  42642  xrlexaddrp  42781  infleinflem2  42800  xrralrecnnge  42820  supminfxr2  42899  xrpnf  42916  icoub  42954  ioonct  42965  ressioosup  42983  ressiooinf  42985  limclner  43082  limsupub  43135  climxrrelem  43180  climlimsupcex  43200  icccncfext  43318  fperdvper  43350  dvdivbd  43354  dvdsn1add  43370  dvmptfprodlem  43375  dvnprodlem3  43379  fourierdlem10  43548  fourierdlem19  43557  fourierdlem20  43558  fourierdlem35  43573  fourierdlem40  43578  fourierdlem41  43579  fourierdlem42  43580  fourierdlem46  43583  fourierdlem48  43585  fourierdlem49  43586  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem68  43605  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem80  43617  elaa2  43665  etransclem35  43700  etransclem38  43703  fge0npnf  43795  sge0tsms  43808  sge0rern  43816  sge0supre  43817  sge0le  43835  sge0fodjrnlem  43844  sge0rpcpnf  43849  meadjun  43890  meadjiunlem  43893  hoidmvlelem2  44024  hspdifhsp  44044  ovolval4lem1  44077