Theorem con2d 134

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 130	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 115	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  135  mt2d  136  pm3.2im  160  exists2  2656  necon2bd  2942  spcimegf  3504  spcegf  3545  spcimedv  3548  rspcimedv  3566  disjxun  5087  exexneq  5375  sotric  5552  sotrieq  5553  poirr2  6068  dfpo2  6239  funun  6523  imadif  6561  soisoi  7257  onnminsb  7727  oneqmin  7728  ordunisuc2  7769  limsssuc  7775  tz7.48lem  8355  sdomdif  9033  sdomdomtrfi  9105  domsdomtrfi  9106  pssinf  9141  unblem1  9171  supnub  9341  infnlb  9372  elirrvOLD  9479  inf3lem6  9518  cantnflem1  9574  cardne  9850  cardsdomel  9859  carddom2  9862  cardmin2  9884  alephnbtwn  9954  infdif2  10092  fin4en1  10192  fin23lem31  10226  isf32lem5  10240  isf34lem4  10260  cfpwsdom  10467  fpwwe2  10526  addnidpi  10784  genpnnp  10888  btwnnz  12541  prime  12546  qsqueeze  13092  xralrple  13096  xmullem2  13156  xmulneg1  13160  ssfzoulel  13652  elfznelfzob  13666  bcval4  14206  seqcoll  14363  hashtpg  14384  swrd0  14558  fsumcvg  15611  fsumsplit  15640  fprodcvg  15829  fprodsplit  15865  dvdsle  16213  divalglem8  16303  bitsinv1lem  16344  2mulprm  16596  pockthg  16810  prmunb  16818  vdwlem6  16890  ramlb  16923  chnpof1  18528  gsumzsplit  19832  obselocv  21658  opsrtoslem2  21984  psdmul  22074  elcls  22981  fbasrn  23792  ufilb  23814  ufilmax  23815  rnelfmlem  23860  alexsubALTlem4  23958  tsmssplit  24060  recld2  24723  logbgcd1irr  26724  fsumharmonic  26942  chtub  27143  lgsne0  27266  sltres  27594  nosupbnd2lem1  27647  nocvxminlem  27710  sltlpss  27846  sltmul2  28103  sltonold  28191  axlowdim  28932  wlkp1lem5  29647  wlkp1lem6  29648  cyclnspth  29772  eupth2lem3lem4  30201  cvnsym  32260  cvntr  32262  atcvati  32356  rmounid  32464  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemfrcn0  34533  ballotlemirc  34535  acycgr2v  35162  cusgracyclt3v  35168  fmlasucdisj  35411  nn0prpw  36336  onsucconni  36450  onint1  36462  icorempo  37364  relowlpssretop  37377  fvineqsneq  37425  lindsenlbs  37634  poimirlem16  37655  poimirlem26  37665  fdc  37764  lsatcvat  39068  hlrelat2  39421  ltltncvr  39441  islln2a  39535  islpln2a  39566  islvol2aN  39610  dvrelog2b  42078  mullt0b2d  42496  rencldnfilem  42832  cantnfresb  43336  dflim5  43341  ss2iundf  43671  uneqsn  44037  radcnvrat  44326  stoweidlem34  46051  oddneven  47654