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

Theorem con2d 131
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 128 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
43con4d 115 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  132  mt2d  133  pm3.2im  158  exists2  2711  necon2bd  2959  spcimegf  3439  spcegf  3441  spcimedv  3444  rspcimedv  3463  disjxun  4785  sotric  5197  sotrieq  5198  poirr2  5662  funun  6076  imadif  6114  soisoi  6722  onnminsb  7152  oneqmin  7153  ordunisuc2  7192  limsssuc  7198  wfrlem10  7578  tz7.48lem  7690  sdomdif  8265  pssinf  8327  unblem1  8369  supnub  8525  infnlb  8555  elirrv  8658  inf3lem6  8695  cantnflem1  8751  cardne  8992  cardsdomel  9001  carddom2  9004  cardmin2  9025  alephnbtwn  9095  infdif2  9235  fin4en1  9334  fin23lem31  9368  isf32lem5  9382  isf34lem4  9402  cfpwsdom  9609  fpwwe2  9668  addnidpi  9926  genpnnp  10030  btwnnz  11656  prime  11661  qsqueeze  12238  xralrple  12242  xmullem2  12301  xmulneg1  12305  ssfzoulel  12771  elfznelfzob  12783  bcval4  13299  seqcoll  13451  hashtpg  13470  swrd0  13644  fsumcvg  14652  fsumsplit  14680  fprodcvg  14868  fprodsplit  14904  dvdsle  15242  divalglem8  15332  bitsinv1lem  15372  pockthg  15818  prmunb  15826  vdwlem6  15898  ramlb  15931  gsumzsplit  18535  opsrtoslem2  19701  obselocv  20290  elcls  21099  fbasrn  21909  ufilb  21931  ufilmax  21932  rnelfmlem  21977  alexsubALTlem4  22075  tsmssplit  22176  recld2  22838  fsumharmonic  24960  chtub  25159  lgsne0  25282  axlowdim  26063  nbgrssovtxOLD  26484  wlkp1lem5  26810  wlkp1lem6  26811  cyclnspth  26932  eupth2lem3lem4  27412  cvnsym  29490  cvntr  29492  atcvati  29586  ballotlemfc0  30895  ballotlemfcc  30896  ballotlemfrcn0  30932  ballotlemirc  30934  dfpo2  31984  sltres  32153  nosupbnd2lem1  32199  nocvxminlem  32231  nn0prpw  32656  onsucconni  32774  onint1  32786  icorempt2  33537  relowlpssretop  33550  lindsenlbs  33738  poimirlem16  33759  poimirlem26  33769  fdc  33874  lsatcvat  34860  hlrelat2  35212  ltltncvr  35232  islln2a  35326  islpln2a  35357  islvol2aN  35401  rencldnfilem  37911  ss2iundf  38478  uneqsn  38848  radcnvrat  39040  stoweidlem34  40769  oddneven  42086
  Copyright terms: Public domain W3C validator