Theorem con2d 128

Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)

Hypothesis

Ref	Expression
con2d.1	⊢ (𝜑 → (𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
con2d	⊢ (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		notnotr 124	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 33	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 113	1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

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  129  mt2d  130  pm3.2im  156  exists2  2550  necon2bd  2798  spcimegf  3260  spcegf  3262  spcimedv  3265  rspcimedv  3284  minelOLD  3986  disjxun  4581  sotric  4985  sotrieq  4986  poirr2  5439  funun  5846  imadif  5887  soisoi  6478  onnminsb  6896  oneqmin  6897  ordunisuc2  6936  limsssuc  6942  wfrlem10  7311  tz7.48lem  7423  sdomdif  7993  pssinf  8055  unblem1  8097  supnub  8251  infnlb  8281  elirrv  8387  inf3lem6  8413  cantnflem1  8469  cardne  8674  cardsdomel  8683  carddom2  8686  cardmin2  8707  alephnbtwn  8777  infdif2  8915  fin4en1  9014  fin23lem31  9048  isf32lem5  9062  isf34lem4  9082  cfpwsdom  9285  fpwwe2  9344  addnidpi  9602  genpnnp  9706  btwnnz  11329  prime  11334  qsqueeze  11906  xralrple  11910  xmullem2  11967  xmulneg1  11971  ssfzoulel  12428  elfznelfzob  12440  bcval4  12956  seqcoll  13105  hashtpg  13121  swrd0  13286  fsumcvg  14290  fsumsplit  14318  fprodcvg  14499  fprodsplit  14535  dvdsle  14870  divalglem8  14961  bitsinv1lem  15001  pockthg  15448  prmunb  15456  vdwlem6  15528  ramlb  15561  gsumzsplit  18150  opsrtoslem2  19306  obselocv  19891  elcls  20687  fbasrn  21498  ufilb  21520  ufilmax  21521  rnelfmlem  21566  alexsubALTlem4  21664  tsmssplit  21765  recld2  22425  fsumharmonic  24538  chtub  24737  lgsne0  24860  axlowdim  25641  nbusgra  25957  nbgranself  25963  usgrasscusgra  26011  cyclnspth  26159  eupath2lem3  26506  cvnsym  28533  cvntr  28535  atcvati  28629  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemfrcn0  29918  ballotlemirc  29920  dfpo2  30898  sltres  31061  nodenselem5  31084  nocvxminlem  31089  nobndup  31099  nobnddown  31100  nofulllem5  31105  nn0prpw  31488  onsucconi  31606  onint1  31618  icorempt2  32375  relowlpssretop  32388  lindsenlbs  32574  poimirlem16  32595  poimirlem26  32605  fdc  32711  lsatcvat  33355  hlrelat2  33707  ltltncvr  33727  islln2a  33821  islpln2a  33852  islvol2aN  33896  rencldnfilem  36402  ss2iundf  36970  uneqsn  37341  radcnvrat  37535  stoweidlem34  38927  oddneven  40095  nbgrssovtx  40586  1wlkp1lem5  40886  1wlkp1lem6  40887  cyclnsPth  41006  eupth2lem3lem4  41399