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  3662  eqsnuniex  5297  onnseq  8259  oeeulem  8511  disjen  9042  cantnflem1  9574  ssfin4  10193  fin1a2lem12  10294  fin1a2lem13  10295  canthnumlem  10531  canthwelem  10533  supaddc  12081  supmul1  12083  ixxdisj  13252  ixxub  13258  ixxlb  13259  icodisj  13368  discr1  14138  01sqrexlem7  15147  bitsfzolem  16337  bitsfzo  16338  sqnprm  16605  mreexexlem2d  17543  acsinfd  18454  simpgntrivd  20005  prmgrpsimpgd  20021  ablsimpgprmd  20022  ornglmullt  20777  orngrmullt  20778  lbsextlem3  21090  lbsextlem4  21091  iunconn  23336  dissnlocfin  23437  ptcmplem4  23963  iccntr  24730  evth  24878  bcthlem5  25248  ovolicopnf  25445  vitalilem4  25532  dvferm1  25909  dvferm2  25911  dgreq0  26191  radcnvle  26349  isosctrlem2  26749  dmlogdmgm  26954  mersenne  27158  2sqn0  27365  pntlem3  27540  ostth2lem1  27549  tgbtwnne  28461  tglowdim1i  28472  tgbtwndiff  28477  tgbtwnconn1lem3  28545  legso  28570  tglineintmo  28613  tglineneq  28615  tglowdim2ln  28622  mirne  28638  mirhl  28650  krippenlem  28661  midexlem  28663  footexALT  28689  footexlem2  28691  colperpexlem3  28703  mideulem2  28705  opphllem  28706  oppnid  28717  opphllem2  28719  outpasch  28726  hlpasch  28727  hpgerlem  28736  colhp  28741  trgcopy  28775  tgasa1  28829  umgrnloop2  29117  ex-natded5.5  30380  ex-natded5.8  30383  ex-natded5.13  30385  unidifsnne  32506  ifnefals  32518  rexmul2  32727  hashpss  32781  nn0min  32793  ccatws1f1o  32922  elrgspnlem2  33200  fracfld  33264  0nellinds  33325  pidlnz  33331  drngidl  33388  drngidlhash  33389  0ringprmidl  33404  qsidomlem1  33407  mxidlirredi  33426  krull  33434  qsdrngi  33450  qsdrng  33452  rsprprmprmidlb  33478  rprmasso2  33481  1arithidom  33492  pidufd  33498  1arithufdlem3  33501  dfufd2  33505  0ringmon1p  33510  ig1pnunit  33551  esplyfv  33581  exsslsb  33599  lvecdim0  33609  lindsunlem  33627  assafld  33640  fldextrspundgdvdslem  33683  extdgfialglem1  33695  irredminply  33719  constrextdg2lem  33751  constrext2chnlem  33753  2sqr3nconstr  33784  cos9thpinconstrlem2  33793  zarcls1  33872  zarclsint  33875  qqhre  34023  esumcvgre  34094  carsgclctunlem2  34322  oddpwdc  34357  eulerpartlemf  34373  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemimin  34509  ballotlem1c  34511  reprinfz1  34625  bnj1417  35043  unbdqndv2lem2  36523  knoppndvlem13  36537  irrdiff  37339  topdifinffinlem  37360  pibt2  37430  poimirlem11  37650  poimirlem12  37651  aks4d1p7  42095  aks4d1p8d2  42097  aks4d1p8  42099  aks4d1p9  42100  fldhmf1  42102  hashscontpow1  42133  aks6d1c5  42151  imo72b2  44184  iunconnlem2  44946  n0p  45061  uzwo4  45069  ssnct  45093  nsstr  45111  disjrnmpt2  45204  difmap  45223  difmapsn  45228  mapssbi  45229  xrlexaddrp  45370  infleinflem2  45388  xrralrecnnge  45407  supminfxr2  45486  xrpnf  45502  icoub  45545  ioonct  45556  ressioosup  45574  ressiooinf  45576  limclner  45668  limsupub  45721  climxrrelem  45766  climlimsupcex  45786  icccncfext  45904  fperdvper  45936  dvdivbd  45940  dvdsn1add  45956  dvmptfprodlem  45961  dvnprodlem3  45965  fourierdlem10  46134  fourierdlem19  46143  fourierdlem20  46144  fourierdlem35  46159  fourierdlem40  46164  fourierdlem41  46165  fourierdlem42  46166  fourierdlem46  46169  fourierdlem48  46171  fourierdlem49  46172  fourierdlem57  46180  fourierdlem58  46181  fourierdlem59  46182  fourierdlem63  46186  fourierdlem64  46187  fourierdlem65  46188  fourierdlem68  46191  fourierdlem74  46197  fourierdlem75  46198  fourierdlem78  46201  fourierdlem79  46202  fourierdlem80  46203  elaa2  46251  etransclem35  46286  etransclem38  46289  fge0npnf  46384  sge0tsms  46397  sge0rern  46405  sge0supre  46406  sge0le  46424  sge0fodjrnlem  46433  sge0rpcpnf  46438  meadjun  46479  meadjiunlem  46482  hoidmvlelem2  46613  hspdifhsp  46633  ovolval4lem1  46666