Theorem pm2.65da 815

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 415	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 415	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 198	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 209  df-an 399

This theorem is referenced by:  condan  816  nelrdva  3696  onnseq  7981  oeeulem  8227  disjen  8674  cantnflem1  9152  ssfin4  9732  fin1a2lem12  9833  fin1a2lem13  9834  canthnumlem  10070  canthwelem  10072  supaddc  11608  supmul1  11610  ixxdisj  12754  ixxub  12760  ixxlb  12761  icodisj  12863  discr1  13601  sqrlem7  14608  bitsfzolem  15783  bitsfzo  15784  sqnprm  16046  mreexexlem2d  16916  acsinfd  17790  simpgntrivd  19220  prmgrpsimpgd  19236  ablsimpgprmd  19237  lbsextlem3  19932  lbsextlem4  19933  iunconn  22036  dissnlocfin  22137  ptcmplem4  22663  iccntr  23429  evth  23563  bcthlem5  23931  ovolicopnf  24125  vitalilem4  24212  dvferm1  24582  dvferm2  24584  dgreq0  24855  radcnvle  25008  isosctrlem2  25397  dmlogdmgm  25601  mersenne  25803  2sqn0  26010  pntlem3  26185  ostth2lem1  26194  tgbtwnne  26276  tglowdim1i  26287  tgbtwndiff  26292  tgbtwnconn1lem3  26360  legso  26385  tglineintmo  26428  tglineneq  26430  tglowdim2ln  26437  mirne  26453  mirhl  26465  krippenlem  26476  midexlem  26478  footexALT  26504  footexlem2  26506  colperpexlem3  26518  mideulem2  26520  opphllem  26521  oppnid  26532  opphllem2  26534  outpasch  26541  hlpasch  26542  hpgerlem  26551  colhp  26556  trgcopy  26590  tgasa1  26644  umgrnloop2  26931  ex-natded5.5  28189  ex-natded5.8  28192  ex-natded5.13  28194  unidifsnne  30296  nn0min  30536  ornglmullt  30880  orngrmullt  30881  0nellinds  30935  qsidomlem1  30965  krull  30980  lvecdim0  31005  lindsunlem  31020  qqhre  31261  esumcvgre  31350  carsgclctunlem2  31577  oddpwdc  31612  eulerpartlemf  31628  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemimin  31763  ballotlem1c  31765  reprinfz1  31893  bnj1417  32313  unbdqndv2lem2  33849  knoppndvlem13  33863  topdifinffinlem  34631  pibt2  34701  poimirlem11  34918  poimirlem12  34919  imo72b2  40545  iunconnlem2  41289  n0p  41325  uzwo4  41335  ssnct  41361  nsstr  41381  disjrnmpt2  41469  difmap  41490  difmapsn  41495  mapssbi  41496  xrlexaddrp  41640  infleinflem2  41659  xrralrecnnge  41682  supminfxr2  41765  xrpnf  41782  icoub  41822  ioonct  41833  ressioosup  41851  ressiooinf  41853  limclner  41952  limsupub  42005  climxrrelem  42050  climlimsupcex  42070  icccncfext  42190  fperdvper  42223  dvdivbd  42228  dvdsn1add  42244  dvmptfprodlem  42249  dvnprodlem3  42253  fourierdlem10  42422  fourierdlem19  42431  fourierdlem20  42432  fourierdlem35  42447  fourierdlem40  42452  fourierdlem41  42453  fourierdlem42  42454  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem57  42468  fourierdlem58  42469  fourierdlem59  42470  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem68  42479  fourierdlem74  42485  fourierdlem75  42486  fourierdlem78  42489  fourierdlem79  42490  fourierdlem80  42491  elaa2  42539  etransclem35  42574  etransclem38  42577  fge0npnf  42669  sge0tsms  42682  sge0rern  42690  sge0supre  42691  sge0le  42709  sge0fodjrnlem  42718  sge0rpcpnf  42723  meadjun  42764  meadjiunlem  42767  hoidmvlelem2  42898  hspdifhsp  42918  ovolval4lem1  42951