MPE Home 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  2549  necon2bd  2797  spcimegf  3259  spcegf  3261  spcimedv  3264  rspcimedv  3283  minelOLD  3985  disjxun  4575  sotric  4975  sotrieq  4976  poirr2  5426  funun  5832  imadif  5873  soisoi  6456  onnminsb  6873  oneqmin  6874  ordunisuc2  6913  limsssuc  6919  wfrlem10  7288  tz7.48lem  7400  sdomdif  7970  pssinf  8032  unblem1  8074  supnub  8228  infnlb  8258  elirrv  8364  inf3lem6  8390  cantnflem1  8446  cardne  8651  cardsdomel  8660  carddom2  8663  cardmin2  8684  alephnbtwn  8754  infdif2  8892  fin4en1  8991  fin23lem31  9025  isf32lem5  9039  isf34lem4  9059  cfpwsdom  9262  fpwwe2  9321  addnidpi  9579  genpnnp  9683  btwnnz  11285  prime  11290  qsqueeze  11865  xralrple  11869  xmullem2  11924  xmulneg1  11928  ssfzoulel  12383  elfznelfzob  12395  bcval4  12911  seqcoll  13057  hashtpg  13071  swrd0  13232  fsumcvg  14236  fsumsplit  14264  fprodcvg  14445  fprodsplit  14481  dvdsle  14816  divalglem8  14907  bitsinv1lem  14947  pockthg  15394  prmunb  15402  vdwlem6  15474  ramlb  15507  gsumzsplit  18096  opsrtoslem2  19252  obselocv  19833  elcls  20629  fbasrn  21440  ufilb  21462  ufilmax  21463  rnelfmlem  21508  alexsubALTlem4  21606  tsmssplit  21707  recld2  22357  fsumharmonic  24455  chtub  24654  lgsne0  24777  axlowdim  25559  nbusgra  25723  nbgranself  25729  usgrasscusgra  25777  cyclnspth  25925  eupath2lem3  26272  cvnsym  28339  cvntr  28341  atcvati  28435  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemfrcn0  29724  ballotlemirc  29726  dfpo2  30704  sltres  30867  nodenselem5  30890  nocvxminlem  30895  nobndup  30905  nobnddown  30906  nofulllem5  30911  nn0prpw  31294  onsucconi  31412  onint1  31424  icorempt2  32178  relowlpssretop  32191  lindsenlbs  32377  poimirlem16  32398  poimirlem26  32408  fdc  32514  lsatcvat  33158  hlrelat2  33510  ltltncvr  33530  islln2a  33624  islpln2a  33655  islvol2aN  33699  rencldnfilem  36205  ss2iundf  36773  uneqsn  37144  radcnvrat  37338  stoweidlem34  38731  oddneven  39900  nbgrssovtx  40588  1wlkp1lem5  40888  1wlkp1lem6  40889  cyclnsPth  41008  eupth2lem3lem4  41401
  Copyright terms: Public domain W3C validator