MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.65da Structured version   Visualization version   GIF version

Theorem pm2.65da 813
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
StepHypRef Expression
1 pm2.65da.1 . . 3 ((𝜑𝜓) → 𝜒)
21ex 413 . 2 (𝜑 → (𝜓𝜒))
3 pm2.65da.2 . . 3 ((𝜑𝜓) → ¬ 𝜒)
43ex 413 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
52, 4pm2.65d 197 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  condan  814  nelrdva  3695  onnseq  7972  oeeulem  8217  disjen  8663  cantnflem1  9141  ssfin4  9721  fin1a2lem12  9822  fin1a2lem13  9823  canthnumlem  10059  canthwelem  10061  supaddc  11597  supmul1  11599  ixxdisj  12743  ixxub  12749  ixxlb  12750  icodisj  12852  discr1  13590  sqrlem7  14598  bitsfzolem  15773  bitsfzo  15774  sqnprm  16036  mreexexlem2d  16906  acsinfd  17780  simpgntrivd  19151  prmgrpsimpgd  19167  ablsimpgprmd  19168  lbsextlem3  19863  lbsextlem4  19864  iunconn  21966  dissnlocfin  22067  ptcmplem4  22593  iccntr  23358  evth  23492  bcthlem5  23860  ovolicopnf  24054  vitalilem4  24141  dvferm1  24511  dvferm2  24513  dgreq0  24784  radcnvle  24937  isosctrlem2  25324  dmlogdmgm  25529  mersenne  25731  2sqn0  25938  pntlem3  26113  ostth2lem1  26122  tgbtwnne  26204  tglowdim1i  26215  tgbtwndiff  26220  tgbtwnconn1lem3  26288  legso  26313  tglineintmo  26356  tglineneq  26358  tglowdim2ln  26365  mirne  26381  mirhl  26393  krippenlem  26404  midexlem  26406  footexALT  26432  footexlem2  26434  colperpexlem3  26446  mideulem2  26448  opphllem  26449  oppnid  26460  opphllem2  26462  outpasch  26469  hlpasch  26470  hpgerlem  26479  colhp  26484  trgcopy  26518  tgasa1  26572  umgrnloop2  26859  ex-natded5.5  28117  ex-natded5.8  28120  ex-natded5.13  28122  unidifsnne  30224  nn0min  30464  ornglmullt  30808  orngrmullt  30809  0nellinds  30863  qsidomlem1  30883  lvecdim0  30905  lindsunlem  30920  qqhre  31161  esumcvgre  31250  carsgclctunlem2  31477  oddpwdc  31512  eulerpartlemf  31528  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemimin  31663  ballotlem1c  31665  reprinfz1  31793  bnj1417  32211  unbdqndv2lem2  33747  knoppndvlem13  33761  topdifinffinlem  34511  pibt2  34581  poimirlem11  34785  poimirlem12  34786  imo72b2  40406  iunconnlem2  41149  n0p  41185  uzwo4  41195  ssnct  41221  nsstr  41241  disjrnmpt2  41329  difmap  41350  difmapsn  41355  mapssbi  41356  xrlexaddrp  41500  infleinflem2  41519  xrralrecnnge  41542  supminfxr2  41625  xrpnf  41642  icoub  41682  ioonct  41693  ressioosup  41711  ressiooinf  41713  limclner  41812  limsupub  41865  climxrrelem  41910  climlimsupcex  41930  icccncfext  42050  fperdvper  42083  dvdivbd  42088  dvdsn1add  42104  dvmptfprodlem  42109  dvnprodlem3  42113  fourierdlem10  42283  fourierdlem19  42292  fourierdlem20  42293  fourierdlem35  42308  fourierdlem40  42313  fourierdlem41  42314  fourierdlem42  42315  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem57  42329  fourierdlem58  42330  fourierdlem59  42331  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem68  42340  fourierdlem74  42346  fourierdlem75  42347  fourierdlem78  42350  fourierdlem79  42351  fourierdlem80  42352  elaa2  42400  etransclem35  42435  etransclem38  42438  fge0npnf  42530  sge0tsms  42543  sge0rern  42551  sge0supre  42552  sge0le  42570  sge0fodjrnlem  42579  sge0rpcpnf  42584  meadjun  42625  meadjiunlem  42628  hoidmvlelem2  42759  hspdifhsp  42779  ovolval4lem1  42812
  Copyright terms: Public domain W3C validator