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  3676  eqsnuniex  5316  onnseq  8313  oeeulem  8565  disjen  9098  cantnflem1  9642  ssfin4  10263  fin1a2lem12  10364  fin1a2lem13  10365  canthnumlem  10601  canthwelem  10603  supaddc  12150  supmul1  12152  ixxdisj  13321  ixxub  13327  ixxlb  13328  icodisj  13437  discr1  14204  01sqrexlem7  15214  bitsfzolem  16404  bitsfzo  16405  sqnprm  16672  mreexexlem2d  17606  acsinfd  18515  simpgntrivd  20030  prmgrpsimpgd  20046  ablsimpgprmd  20047  lbsextlem3  21070  lbsextlem4  21071  iunconn  23315  dissnlocfin  23416  ptcmplem4  23942  iccntr  24710  evth  24858  bcthlem5  25228  ovolicopnf  25425  vitalilem4  25512  dvferm1  25889  dvferm2  25891  dgreq0  26171  radcnvle  26329  isosctrlem2  26729  dmlogdmgm  26934  mersenne  27138  2sqn0  27345  pntlem3  27520  ostth2lem1  27529  tgbtwnne  28417  tglowdim1i  28428  tgbtwndiff  28433  tgbtwnconn1lem3  28501  legso  28526  tglineintmo  28569  tglineneq  28571  tglowdim2ln  28578  mirne  28594  mirhl  28606  krippenlem  28617  midexlem  28619  footexALT  28645  footexlem2  28647  colperpexlem3  28659  mideulem2  28661  opphllem  28662  oppnid  28673  opphllem2  28675  outpasch  28682  hlpasch  28683  hpgerlem  28692  colhp  28697  trgcopy  28731  tgasa1  28785  umgrnloop2  29073  ex-natded5.5  30339  ex-natded5.8  30342  ex-natded5.13  30344  unidifsnne  32465  ifnefals  32477  rexmul2  32677  hashpss  32734  nn0min  32745  ccatws1f1o  32873  elrgspnlem2  33194  fracfld  33258  ornglmullt  33285  orngrmullt  33286  0nellinds  33341  pidlnz  33347  drngidl  33404  drngidlhash  33405  0ringprmidl  33420  qsidomlem1  33423  mxidlirredi  33442  krull  33450  qsdrngi  33466  qsdrng  33468  rsprprmprmidlb  33494  rprmasso2  33497  1arithidom  33508  pidufd  33514  1arithufdlem3  33517  dfufd2  33521  0ringmon1p  33526  ig1pnunit  33566  exsslsb  33592  lvecdim0  33602  lindsunlem  33620  assafld  33633  fldextrspundgdvdslem  33675  irredminply  33706  constrextdg2lem  33738  constrext2chnlem  33740  2sqr3nconstr  33771  cos9thpinconstrlem2  33780  zarcls1  33859  zarclsint  33862  qqhre  34010  esumcvgre  34081  carsgclctunlem2  34310  oddpwdc  34345  eulerpartlemf  34361  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemimin  34497  ballotlem1c  34499  reprinfz1  34613  bnj1417  35031  unbdqndv2lem2  36498  knoppndvlem13  36512  irrdiff  37314  topdifinffinlem  37335  pibt2  37405  poimirlem11  37625  poimirlem12  37626  aks4d1p7  42071  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  fldhmf1  42078  hashscontpow1  42109  aks6d1c5  42127  imo72b2  44161  iunconnlem2  44924  n0p  45039  uzwo4  45047  ssnct  45071  nsstr  45089  disjrnmpt2  45182  difmap  45201  difmapsn  45206  mapssbi  45207  xrlexaddrp  45348  infleinflem2  45367  xrralrecnnge  45386  supminfxr2  45465  xrpnf  45481  icoub  45524  ioonct  45535  ressioosup  45553  ressiooinf  45555  limclner  45649  limsupub  45702  climxrrelem  45747  climlimsupcex  45767  icccncfext  45885  fperdvper  45917  dvdivbd  45921  dvdsn1add  45937  dvmptfprodlem  45942  dvnprodlem3  45946  fourierdlem10  46115  fourierdlem19  46124  fourierdlem20  46125  fourierdlem35  46140  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem57  46161  fourierdlem58  46162  fourierdlem59  46163  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem68  46172  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem80  46184  elaa2  46232  etransclem35  46267  etransclem38  46270  fge0npnf  46365  sge0tsms  46378  sge0rern  46386  sge0supre  46387  sge0le  46405  sge0fodjrnlem  46414  sge0rpcpnf  46419  meadjun  46460  meadjiunlem  46463  hoidmvlelem2  46594  hspdifhsp  46614  ovolval4lem1  46647