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  2687  necon2bd  2972  spcimegf  3518  spcegf  3550  spcimedv  3553  rspcimedv  3571  disjxun  5106  exexneq  5416  sotric  5599  sotrieq  5600  poirr2  6124  dfpo2  6297  funun  6582  imadif  6620  soisoi  7326  onnminsb  7797  oneqmin  7798  ordunisuc2  7839  limsssuc  7845  tz7.48lem  8427  sdomdif  9112  sdomdomtrfi  9184  domsdomtrfi  9185  pssinf  9221  unblem1  9251  supnub  9421  infnlb  9452  elirrv  9558  elirrvOLDOLD  9560  inf3lem6  9601  cantnflem1  9657  cardne  9950  cardsdomel  9959  carddom2  9962  cardmin2  9984  alephnbtwn  10054  infdif2  10191  fin4en1  10292  fin23lem31  10326  isf32lem5  10340  isf34lem4  10360  cfpwsdom  10568  fpwwe2  10627  addnidpi  10885  genpnnp  10989  btwnnz  12671  prime  12676  qsqueeze  13226  xralrple  13230  xmullem2  13290  xmulneg1  13294  ssfzoulel  13789  elfznelfzob  13803  bcval4  14343  seqcoll  14501  hashtpg  14522  swrd0  14696  fsumcvg  15763  fsumsplit  15792  fprodcvg  15984  fprodsplit  16020  dvdsle  16367  divalglem8  16457  bitsinv1lem  16498  2mulprm  16750  pockthg  16965  prmunb  16973  vdwlem6  17045  ramlb  17078  chnpof1  18685  gsumzsplit  19996  obselocv  21857  opsrtoslem2  22186  psdmul  22308  elcls  23209  fbasrn  24020  ufilb  24042  ufilmax  24043  rnelfmlem  24088  alexsubALTlem4  24186  tsmssplit  24288  recld2  24951  logbgcd1irr  26935  fsumharmonic  27152  chtub  27352  lgsne0  27475  ltsres  27802  nosupbnd2lem1  27855  nocvxminlem  27923  ltslpss  28077  ltmuls2  28340  ltonold  28430  axlowdim  29277  wlkp1lem5  29991  wlkp1lem6  29992  cyclnspth  30116  eupth2lem3lem4  30548  cvnsym  32608  cvntr  32610  atcvati  32704  rmounid  32807  ballotlemfc0  34849  ballotlemfcc  34850  ballotlemfrcn0  34886  ballotlemirc  34888  acycgr2v  35608  cusgracyclt3v  35614  fmlasucdisj  35857  nmulprop  36648  nn0prpw  36800  onsucconni  36914  onint1  36926  icorempo  37963  relowlpssretop  37976  fvineqsneq  38024  lindsenlbs  38232  poimirlem16  38253  poimirlem26  38263  fdc  38362  lsatcvat  39792  hlrelat2  40145  ltltncvr  40165  islln2a  40259  islpln2a  40290  islvol2aN  40334  dvrelog2b  42801  mullt0b2d  43226  rencldnfilem  43517  cantnfresb  44021  dflim5  44026  ss2iundf  44355  uneqsn  44721  radcnvrat  44994  stoweidlem34  46718  oddneven  48376