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

Theorem con2d 127
 Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
con2d (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d
StepHypRef Expression
1 notnotr 123 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 33 . 2 (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
43con4d 112 1 (𝜑 → (𝜒 → ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem is referenced by:  con2  128  mt2d  129  pm3.2im  155  exists2  2454  necon2bd  2702  spcimegf  3164  spcegf  3166  spcimedv  3169  rspcimedv  3188  minelOLD  3889  disjxun  4479  sotric  4879  sotrieq  4880  poirr2  5330  funun  5736  imadif  5777  soisoi  6360  onnminsb  6777  oneqmin  6778  ordunisuc2  6817  limsssuc  6823  wfrlem10  7191  tz7.48lem  7303  sdomdif  7873  pssinf  7935  unblem1  7977  supnub  8131  infnlb  8161  elirrv  8267  inf3lem6  8293  cantnflem1  8349  cardne  8554  cardsdomel  8563  carddom2  8566  cardmin2  8587  alephnbtwn  8657  infdif2  8795  fin4en1  8894  fin23lem31  8928  isf32lem5  8942  isf34lem4  8962  cfpwsdom  9165  fpwwe2  9224  addnidpi  9482  genpnnp  9586  btwnnz  11197  prime  11202  qsqueeze  11779  xralrple  11783  xmullem2  11838  xmulneg1  11842  ssfzoulel  12300  elfznelfzob  12312  bcval4  12828  seqcoll  12974  hashtpg  12988  swrd0  13149  fsumcvg  14163  fsumsplit  14191  fprodcvg  14372  fprodsplit  14408  dvdsle  14743  divalglem8  14836  bitsinv1lem  14878  pockthg  15336  prmunb  15344  vdwlem6  15416  ramlb  15449  gsumzsplit  18061  opsrtoslem2  19214  obselocv  19798  elcls  20594  fbasrn  21405  ufilb  21427  ufilmax  21428  rnelfmlem  21473  alexsubALTlem4  21571  tsmssplit  21672  recld2  22338  fsumharmonic  24429  chtub  24630  lgsne0  24753  axlowdim  25535  nbusgra  25699  nbgranself  25705  usgrasscusgra  25753  cyclnspth  25901  eupath2lem3  26248  cvnsym  28325  cvntr  28327  atcvati  28421  ballotlemfc0  29692  ballotlemfcc  29693  ballotlemfrcn0  29729  ballotlemirc  29731  ballotlemfrcn0OLD  29767  ballotlemircOLD  29769  dfpo2  30744  sltres  30900  nodenselem5  30923  nocvxminlem  30928  nobndup  30938  nobnddown  30939  nofulllem5  30944  nn0prpw  31326  onsucconi  31444  onint1  31456  icorempt2  32210  relowlpssretop  32223  lindsenlbs  32468  poimirlem16  32489  poimirlem26  32499  fdc  32605  lsatcvat  33249  hlrelat2  33601  ltltncvr  33621  islln2a  33715  islpln2a  33746  islvol2aN  33790  rencldnfilem  36296  ss2iundf  36871  uneqsn  37242  radcnvrat  37436  stoweidlem34  38834  oddneven  40007  nbgrssovtx  40695  1wlkp1lem5  40995  1wlkp1lem6  40996  cyclnsPth  41115  eupth2lem3lem4  41508
 Copyright terms: Public domain W3C validator