Theorem pm2.65da 828

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  condan  829  nelrdva  3667  eqsnuniex  5331  onnseq  8329  oeeulem  8585  disjen  9120  cantnflem1  9656  ssfin4  10300  fin1a2lem12  10401  fin1a2lem13  10402  canthnumlem  10639  canthwelem  10641  supaddc  12188  supmul1  12190  ixxdisj  13393  ixxub  13399  ixxlb  13400  icodisj  13509  discr1  14282  hashpss  14453  01sqrexlem7  15306  bitsfzolem  16498  bitsfzo  16499  sqnprm  16767  mreexexlem2d  17707  acsinfd  18618  simpgntrivd  20176  prmgrpsimpgd  20192  ablsimpgprmd  20193  ornglmullt  20983  orngrmullt  20984  lbsextlem3  21295  lbsextlem4  21296  pidlnz  21385  drngidl  21396  0ringprmidl  21488  qsidomlem1  21491  iunconn  23596  dissnlocfin  23697  ptcmplem4  24223  iccntr  24990  evth  25129  bcthlem5  25498  ovolicopnf  25694  vitalilem4  25781  dvferm1  26155  dvferm2  26157  dgreq0  26433  radcnvle  26594  isosctrlem2  26995  dmlogdmgm  27199  mersenne  27402  2sqn0  27609  pntlem3  27784  ostth2lem1  27793  tgbtwnne  28770  tglowdim1i  28781  tgbtwndiff  28786  tgbtwnconn1lem3  28854  legso  28879  tglineintmo  28926  tglineneq  28929  tglowdim2ln  28936  tglnpt4  28939  mirne  28955  mirhl  28967  krippenlem  28978  midexlem  28980  symquadprlnglem  28981  footexALT  29009  footexlem2  29011  colperpexlem3  29024  mideulem2  29026  opphllem  29027  oppnid  29038  opphllem2  29040  outpasch  29048  hlpasch  29049  hpgerlem  29058  colhp  29063  trgcopy  29126  tgasa1  29186  prlnghpg  29207  prlngmolem1  29213  prlngmolem2  29214  prlngpln4  29219  prlngsymquadlem  29224  umgrnloop2  29507  ex-natded5.5  30772  ex-natded5.8  30775  ex-natded5.13  30777  unidifsnne  32893  ifnefals  32905  rexmul2  33110  nn0min  33176  ccatws1f1o  33280  elrgspnlem2  33572  fracfld  33638  0nellinds  33694  drngidlhash  33750  mxidlirredi  33763  krull  33770  qsdrngi  33786  qsdrng  33788  rsprprmprmidlb  33822  rprmasso2  33825  1arithidom  33836  pidufd  33842  1arithufdlem3  33845  dfufd2  33849  0ringmon1p  33856  ig1pnunit  33900  mplmulmvr  33938  evlextv  33941  esplyfv  33969  esplyfval1  33972  esplyind  33974  vietadeg1  33977  exsslsb  33996  lvecdim0  34006  lindsunlem  34023  assafld  34036  fldextrspundgdvdslem  34079  extdgfialglem1  34091  irredminply  34115  constrextdg2lem  34147  constrext2chnlem  34149  2sqr3nconstr  34180  cos9thpinconstrlem2  34189  zarcls1  34268  zarclsint  34271  qqhre  34419  esumcvgre  34490  carsgclctunlem2  34718  oddpwdc  34753  eulerpartlemf  34769  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemimin  34905  ballotlem1c  34907  reprinfz1  35018  bnj1417  35438  ttcwf2  37064  unbdqndv2lem2  37127  knoppndvlem13  37141  irrdiff  37998  topdifinffinlem  38021  pibt2  38091  poimirlem11  38310  poimirlem12  38311  aks4d1p7  42878  aks4d1p8d2  42880  aks4d1p8  42882  aks4d1p9  42883  fldhmf1  42885  hashscontpow1  42916  aks6d1c5  42934  imo72b2  44926  iunconnlem2  45671  n0p  45793  uzwo4  45801  ssnct  45825  nsstr  45841  disjrnmpt2  45934  difmap  45951  difmapsn  45956  mapssbi  45957  xrlexaddrp  46096  infleinflem2  46114  xrralrecnnge  46133  supminfxr2  46211  xrpnf  46227  icoub  46270  ioonct  46281  ressioosup  46299  ressiooinf  46301  limclner  46393  limsupub  46446  climxrrelem  46491  climlimsupcex  46511  icccncfext  46629  fperdvper  46661  dvdivbd  46665  dvdsn1add  46681  dvmptfprodlem  46686  dvnprodlem3  46690  fourierdlem10  46859  fourierdlem19  46868  fourierdlem20  46869  fourierdlem35  46884  fourierdlem40  46889  fourierdlem41  46890  fourierdlem42  46891  fourierdlem46  46894  fourierdlem48  46896  fourierdlem49  46897  fourierdlem57  46905  fourierdlem58  46906  fourierdlem59  46907  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem68  46916  fourierdlem74  46922  fourierdlem75  46923  fourierdlem78  46926  fourierdlem79  46927  fourierdlem80  46928  elaa2  46976  etransclem35  47011  etransclem38  47014  fge0npnf  47109  sge0tsms  47122  sge0rern  47130  sge0supre  47131  sge0le  47149  sge0fodjrnlem  47158  sge0rpcpnf  47163  meadjun  47204  meadjiunlem  47207  hoidmvlelem2  47338  hspdifhsp  47358  ovolval4lem1  47391