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

Theorem con2d 129
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 125 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
43con4d 114 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  130  mt2d  131  pm3.2im  157  exists2  2561  necon2bd  2806  spcimegf  3273  spcegf  3275  spcimedv  3278  rspcimedv  3297  minelOLD  4006  disjxun  4611  sotric  5021  sotrieq  5022  poirr2  5479  funun  5890  imadif  5931  soisoi  6532  onnminsb  6951  oneqmin  6952  ordunisuc2  6991  limsssuc  6997  wfrlem10  7369  tz7.48lem  7481  sdomdif  8052  pssinf  8114  unblem1  8156  supnub  8312  infnlb  8342  elirrv  8448  inf3lem6  8474  cantnflem1  8530  cardne  8735  cardsdomel  8744  carddom2  8747  cardmin2  8768  alephnbtwn  8838  infdif2  8976  fin4en1  9075  fin23lem31  9109  isf32lem5  9123  isf34lem4  9143  cfpwsdom  9350  fpwwe2  9409  addnidpi  9667  genpnnp  9771  btwnnz  11397  prime  11402  qsqueeze  11975  xralrple  11979  xmullem2  12038  xmulneg1  12042  ssfzoulel  12503  elfznelfzob  12515  bcval4  13034  seqcoll  13186  hashtpg  13205  swrd0  13372  fsumcvg  14376  fsumsplit  14404  fprodcvg  14585  fprodsplit  14621  dvdsle  14956  divalglem8  15047  bitsinv1lem  15087  pockthg  15534  prmunb  15542  vdwlem6  15614  ramlb  15647  gsumzsplit  18248  opsrtoslem2  19404  obselocv  19991  elcls  20787  fbasrn  21598  ufilb  21620  ufilmax  21621  rnelfmlem  21666  alexsubALTlem4  21764  tsmssplit  21865  recld2  22525  fsumharmonic  24638  chtub  24837  lgsne0  24960  axlowdim  25741  nbgrssovtx  26147  wlkp1lem5  26443  wlkp1lem6  26444  cyclnspth  26564  eupth2lem3lem4  26957  cvnsym  28995  cvntr  28997  atcvati  29091  ballotlemfc0  30332  ballotlemfcc  30333  ballotlemfrcn0  30369  ballotlemirc  30371  dfpo2  31350  sltres  31515  nodenselem5  31545  nocvxminlem  31550  nobndup  31560  nobnddown  31561  nn0prpw  31957  onsucconni  32075  onint1  32087  icorempt2  32828  relowlpssretop  32841  lindsenlbs  33033  poimirlem16  33054  poimirlem26  33064  fdc  33170  lsatcvat  33814  hlrelat2  34166  ltltncvr  34186  islln2a  34280  islpln2a  34311  islvol2aN  34355  rencldnfilem  36861  ss2iundf  37429  uneqsn  37800  radcnvrat  37992  stoweidlem34  39555  oddneven  40853
  Copyright terms: Public domain W3C validator