Theorem pm2.65da 598

Description: Deduction rule 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 449	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		pm2.65da.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)
4	3	ex 449	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
5	2, 4	pm2.65d 186	1 ⊢ (𝜑 → ¬ 𝜓)

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

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 196  df-an 385

This theorem is referenced by:  condan  831  nelrdva  3384  onnseq  7328  oeeulem  7568  disjen  8002  cantnflem1  8469  ssfin4  9015  fin1a2lem12  9116  fin1a2lem13  9117  canthnumlem  9349  canthwelem  9351  supaddc  10867  supmul1  10869  ixxdisj  12061  ixxub  12067  ixxlb  12068  icodisj  12168  discr1  12862  sqrlem7  13837  bitsfzolem  14994  bitsfzo  14995  sqnprm  15252  mreexexlem2d  16128  acsinfd  17003  lbsextlem3  18981  lbsextlem4  18982  iuncon  21041  dissnlocfin  21142  ptcmplem4  21669  iccntr  22432  evth  22566  bcthlem5  22933  ovolicopnf  23099  vitalilem4  23186  dvferm1  23552  dvferm2  23554  dgreq0  23825  radcnvle  23978  isosctrlem2  24349  dmlogdmgm  24550  mersenne  24752  pntlem3  25098  ostth2lem1  25107  tgbtwnne  25185  tglowdim1i  25196  tgbtwndiff  25201  tgbtwnconn1lem3  25269  legso  25294  tglineintmo  25337  tglineneq  25339  tglowdim2ln  25346  mirne  25362  mirhl  25374  krippenlem  25385  midexlem  25387  footex  25413  colperpexlem3  25424  mideulem2  25426  opphllem  25427  oppne3  25435  oppnid  25438  opphllem1  25439  opphllem2  25440  outpasch  25447  hlpasch  25448  hpgerlem  25457  colhp  25462  trgcopy  25496  cgrancol  25520  tgasa1  25539  umgrnloop2  25817  ex-natded5.5  26659  ex-natded5.8  26662  ex-natded5.13  26664  nn0min  28954  2sqn0  28977  ornglmullt  29138  orngrmullt  29139  qqhre  29392  esumcvgre  29480  carsgclctunlem2  29708  oddpwdc  29743  eulerpartlemf  29759  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemimin  29894  ballotlem1c  29896  bnj1417  30363  unbdqndv2lem2  31671  knoppndvlem13  31685  topdifinffinlem  32371  poimirlem11  32590  poimirlem12  32591  imo72b2  37497  iunconlem2  38193  n0p  38234  uzwo4  38246  ssnct  38275  nelpr2  38288  nelpr1  38289  nsstr  38301  disjrnmpt2  38370  difmap  38394  difmapsn  38399  mapssbi  38400  xrlexaddrp  38509  infleinflem2  38528  xrralrecnnge  38554  icoub  38599  ioonct  38611  ressioosup  38629  ressiooinf  38631  limclner  38718  icccncfext  38773  fperdvper  38808  dvdivbd  38813  dvdsn1add  38829  dvmptfprodlem  38834  dvnprodlem3  38838  fourierdlem10  39010  fourierdlem19  39019  fourierdlem20  39020  fourierdlem35  39035  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem68  39067  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem80  39079  elaa2  39127  etransclem35  39162  etransclem38  39165  prsal  39214  fge0npnf  39260  sge0tsms  39273  sge0rern  39281  sge0supre  39282  sge0le  39300  sge0fodjrnlem  39309  sge0rpcpnf  39314  meadjun  39355  meadjiunlem  39358  hoidmvlelem2  39486  hspdifhsp  39506  ovolval4lem1  39539  preimagelt  39589  preimalegt  39590