Theorem pm2.65da 817

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  818  nelrdva  3602  onnseq  8003  oeeulem  8251  disjen  8717  cantnflem1  9218  ssfin4  9803  fin1a2lem12  9904  fin1a2lem13  9905  canthnumlem  10141  canthwelem  10143  supaddc  11678  supmul1  11680  ixxdisj  12829  ixxub  12835  ixxlb  12836  icodisj  12943  discr1  13685  sqrlem7  14691  bitsfzolem  15870  bitsfzo  15871  sqnprm  16136  mreexexlem2d  17012  acsinfd  17899  simpgntrivd  19332  prmgrpsimpgd  19348  ablsimpgprmd  19349  lbsextlem3  20044  lbsextlem4  20045  iunconn  22172  dissnlocfin  22273  ptcmplem4  22799  iccntr  23566  evth  23704  bcthlem5  24073  ovolicopnf  24269  vitalilem4  24356  dvferm1  24729  dvferm2  24731  dgreq0  25006  radcnvle  25159  isosctrlem2  25549  dmlogdmgm  25753  mersenne  25955  2sqn0  26162  pntlem3  26337  ostth2lem1  26346  tgbtwnne  26428  tglowdim1i  26439  tgbtwndiff  26444  tgbtwnconn1lem3  26512  legso  26537  tglineintmo  26580  tglineneq  26582  tglowdim2ln  26589  mirne  26605  mirhl  26617  krippenlem  26628  midexlem  26630  footexALT  26656  footexlem2  26658  colperpexlem3  26670  mideulem2  26672  opphllem  26673  oppnid  26684  opphllem2  26686  outpasch  26693  hlpasch  26694  hpgerlem  26703  colhp  26708  trgcopy  26742  tgasa1  26796  umgrnloop2  27083  ex-natded5.5  28339  ex-natded5.8  28342  ex-natded5.13  28344  unidifsnne  30450  nn0min  30701  ornglmullt  31075  orngrmullt  31076  0nellinds  31130  pidlnz  31135  0ringprmidl  31189  qsidomlem1  31192  krull  31207  lvecdim0  31254  lindsunlem  31269  zarcls1  31383  zarclsint  31386  qqhre  31532  esumcvgre  31621  carsgclctunlem2  31848  oddpwdc  31883  eulerpartlemf  31899  ballotlemfc0  32021  ballotlemfcc  32022  ballotlemimin  32034  ballotlem1c  32036  reprinfz1  32164  bnj1417  32584  unbdqndv2lem2  34320  knoppndvlem13  34334  irrdiff  35106  topdifinffinlem  35130  pibt2  35200  poimirlem11  35400  poimirlem12  35401  imo72b2  41314  iunconnlem2  42077  n0p  42113  uzwo4  42123  ssnct  42149  nsstr  42167  disjrnmpt2  42248  difmap  42269  difmapsn  42274  mapssbi  42275  xrlexaddrp  42413  infleinflem2  42432  xrralrecnnge  42452  supminfxr2  42533  xrpnf  42550  icoub  42588  ioonct  42599  ressioosup  42617  ressiooinf  42619  limclner  42718  limsupub  42771  climxrrelem  42816  climlimsupcex  42836  icccncfext  42954  fperdvper  42986  dvdivbd  42990  dvdsn1add  43006  dvmptfprodlem  43011  dvnprodlem3  43015  fourierdlem10  43184  fourierdlem19  43193  fourierdlem20  43194  fourierdlem35  43209  fourierdlem40  43214  fourierdlem41  43215  fourierdlem42  43216  fourierdlem46  43219  fourierdlem48  43221  fourierdlem49  43222  fourierdlem57  43230  fourierdlem58  43231  fourierdlem59  43232  fourierdlem63  43236  fourierdlem64  43237  fourierdlem65  43238  fourierdlem68  43241  fourierdlem74  43247  fourierdlem75  43248  fourierdlem78  43251  fourierdlem79  43252  fourierdlem80  43253  elaa2  43301  etransclem35  43336  etransclem38  43339  fge0npnf  43431  sge0tsms  43444  sge0rern  43452  sge0supre  43453  sge0le  43471  sge0fodjrnlem  43480  sge0rpcpnf  43485  meadjun  43526  meadjiunlem  43529  hoidmvlelem2  43660  hspdifhsp  43680  ovolval4lem1  43713