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  2691  necon2bd  2976  spcimegf  3522  spcegf  3554  spcimedv  3557  rspcimedv  3575  disjxun  5103  exexneq  5407  sotric  5590  sotrieq  5591  poirr2  6115  dfpo2  6287  funun  6571  imadif  6609  soisoi  7316  onnminsb  7786  oneqmin  7787  ordunisuc2  7828  limsssuc  7834  tz7.48lem  8416  sdomdif  9101  sdomdomtrfi  9173  domsdomtrfi  9174  pssinf  9210  unblem1  9240  supnub  9410  infnlb  9441  elirrv  9547  elirrvOLDOLD  9549  inf3lem6  9590  cantnflem1  9646  cardne  9939  cardsdomel  9948  carddom2  9951  cardmin2  9973  alephnbtwn  10043  infdif2  10180  fin4en1  10281  fin23lem31  10315  isf32lem5  10329  isf34lem4  10349  cfpwsdom  10557  fpwwe2  10616  addnidpi  10874  genpnnp  10978  btwnnz  12663  prime  12668  qsqueeze  13218  xralrple  13222  xmullem2  13282  xmulneg1  13286  ssfzoulel  13780  elfznelfzob  13794  bcval4  14334  seqcoll  14491  hashtpg  14512  swrd0  14686  fsumcvg  15753  fsumsplit  15782  fprodcvg  15974  fprodsplit  16010  dvdsle  16358  divalglem8  16448  bitsinv1lem  16489  2mulprm  16741  pockthg  16956  prmunb  16964  vdwlem6  17036  ramlb  17069  chnpof1  18676  gsumzsplit  19988  obselocv  21838  opsrtoslem2  22167  psdmul  22289  elcls  23191  fbasrn  24002  ufilb  24024  ufilmax  24025  rnelfmlem  24070  alexsubALTlem4  24168  tsmssplit  24270  recld2  24933  logbgcd1irr  26917  fsumharmonic  27134  chtub  27334  lgsne0  27457  ltsres  27784  nosupbnd2lem1  27837  nocvxminlem  27905  ltslpss  28059  ltmuls2  28322  ltonold  28412  axlowdim  29220  wlkp1lem5  29934  wlkp1lem6  29935  cyclnspth  30059  eupth2lem3lem4  30491  cvnsym  32551  cvntr  32553  atcvati  32647  rmounid  32751  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemfrcn0  34837  ballotlemirc  34839  acycgr2v  35513  cusgracyclt3v  35519  fmlasucdisj  35762  nmulprop  36553  nn0prpw  36696  onsucconni  36810  onint1  36822  icorempo  37857  relowlpssretop  37870  fvineqsneq  37918  lindsenlbs  38126  poimirlem16  38147  poimirlem26  38157  fdc  38256  lsatcvat  39686  hlrelat2  40039  ltltncvr  40059  islln2a  40153  islpln2a  40184  islvol2aN  40228  dvrelog2b  42695  mullt0b2d  43118  rencldnfilem  43409  cantnfresb  43913  dflim5  43918  ss2iundf  44247  uneqsn  44613  radcnvrat  44888  stoweidlem34  46606  oddneven  48264