Theorem con2d 135

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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 116	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  136  mt2d  137  pm3.2im  161  exists2  2695  necon2bd  2980  spcimegf  3526  spcegf  3558  spcimedv  3561  rspcimedv  3579  disjxun  5109  exexneq  5417  sotric  5600  sotrieq  5601  poirr2  6125  dfpo2  6298  funun  6583  imadif  6621  soisoi  7327  onnminsb  7798  oneqmin  7799  ordunisuc2  7840  limsssuc  7846  tz7.48lem  8428  sdomdif  9113  sdomdomtrfi  9185  domsdomtrfi  9186  pssinf  9222  unblem1  9252  supnub  9422  infnlb  9453  elirrv  9559  elirrvOLDOLD  9561  inf3lem6  9602  cantnflem1  9658  cardne  9951  cardsdomel  9960  carddom2  9963  cardmin2  9985  alephnbtwn  10055  infdif2  10192  fin4en1  10293  fin23lem31  10327  isf32lem5  10341  isf34lem4  10361  cfpwsdom  10569  fpwwe2  10628  addnidpi  10886  genpnnp  10990  btwnnz  12672  prime  12677  qsqueeze  13227  xralrple  13231  xmullem2  13291  xmulneg1  13295  ssfzoulel  13789  elfznelfzob  13803  bcval4  14343  seqcoll  14501  hashtpg  14522  swrd0  14696  fsumcvg  15763  fsumsplit  15792  fprodcvg  15984  fprodsplit  16020  dvdsle  16368  divalglem8  16458  bitsinv1lem  16499  2mulprm  16751  pockthg  16966  prmunb  16974  vdwlem6  17046  ramlb  17079  chnpof1  18686  gsumzsplit  19997  obselocv  21847  opsrtoslem2  22176  psdmul  22298  elcls  23199  fbasrn  24010  ufilb  24032  ufilmax  24033  rnelfmlem  24078  alexsubALTlem4  24176  tsmssplit  24278  recld2  24941  logbgcd1irr  26925  fsumharmonic  27142  chtub  27342  lgsne0  27465  ltsres  27792  nosupbnd2lem1  27845  nocvxminlem  27913  ltslpss  28067  ltmuls2  28330  ltonold  28420  axlowdim  29252  wlkp1lem5  29966  wlkp1lem6  29967  cyclnspth  30091  eupth2lem3lem4  30523  cvnsym  32583  cvntr  32585  atcvati  32679  rmounid  32782  ballotlemfc0  34828  ballotlemfcc  34829  ballotlemfrcn0  34865  ballotlemirc  34867  acycgr2v  35575  cusgracyclt3v  35581  fmlasucdisj  35824  nmulprop  36615  nn0prpw  36757  onsucconni  36871  onint1  36883  icorempo  37920  relowlpssretop  37933  fvineqsneq  37981  lindsenlbs  38189  poimirlem16  38210  poimirlem26  38220  fdc  38319  lsatcvat  39749  hlrelat2  40102  ltltncvr  40122  islln2a  40216  islpln2a  40247  islvol2aN  40291  dvrelog2b  42758  mullt0b2d  43183  rencldnfilem  43474  cantnfresb  43978  dflim5  43983  ss2iundf  44312  uneqsn  44678  radcnvrat  44951  stoweidlem34  46675  oddneven  48333