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  2663  necon2bd  2949  spcimegf  3509  spcegf  3547  spcimedv  3550  rspcimedv  3568  disjxun  5097  exexneq  5385  sotric  5563  sotrieq  5564  poirr2  6082  dfpo2  6255  funun  6539  imadif  6577  soisoi  7276  onnminsb  7746  oneqmin  7747  ordunisuc2  7788  limsssuc  7794  tz7.48lem  8374  sdomdif  9057  sdomdomtrfi  9129  domsdomtrfi  9130  pssinf  9166  unblem1  9196  supnub  9369  infnlb  9400  elirrvOLD  9507  inf3lem6  9546  cantnflem1  9602  cardne  9881  cardsdomel  9890  carddom2  9893  cardmin2  9915  alephnbtwn  9985  infdif2  10123  fin4en1  10223  fin23lem31  10257  isf32lem5  10271  isf34lem4  10291  cfpwsdom  10499  fpwwe2  10558  addnidpi  10816  genpnnp  10920  btwnnz  12572  prime  12577  qsqueeze  13120  xralrple  13124  xmullem2  13184  xmulneg1  13188  ssfzoulel  13680  elfznelfzob  13694  bcval4  14234  seqcoll  14391  hashtpg  14412  swrd0  14586  fsumcvg  15639  fsumsplit  15668  fprodcvg  15857  fprodsplit  15893  dvdsle  16241  divalglem8  16331  bitsinv1lem  16372  2mulprm  16624  pockthg  16838  prmunb  16846  vdwlem6  16918  ramlb  16951  chnpof1  18557  gsumzsplit  19860  obselocv  21687  opsrtoslem2  22015  psdmul  22113  elcls  23021  fbasrn  23832  ufilb  23854  ufilmax  23855  rnelfmlem  23900  alexsubALTlem4  23998  tsmssplit  24100  recld2  24763  logbgcd1irr  26764  fsumharmonic  26982  chtub  27183  lgsne0  27306  sltres  27634  nosupbnd2lem1  27687  nocvxminlem  27754  sltlpss  27890  sltmul2  28153  sltonold  28242  axlowdim  29017  wlkp1lem5  29732  wlkp1lem6  29733  cyclnspth  29857  eupth2lem3lem4  30289  cvnsym  32348  cvntr  32350  atcvati  32444  rmounid  32551  ballotlemfc0  34631  ballotlemfcc  34632  ballotlemfrcn0  34668  ballotlemirc  34670  acycgr2v  35325  cusgracyclt3v  35331  fmlasucdisj  35574  nn0prpw  36498  onsucconni  36612  onint1  36624  icorempo  37527  relowlpssretop  37540  fvineqsneq  37588  lindsenlbs  37787  poimirlem16  37808  poimirlem26  37818  fdc  37917  lsatcvat  39347  hlrelat2  39700  ltltncvr  39720  islln2a  39814  islpln2a  39845  islvol2aN  39889  dvrelog2b  42357  mullt0b2d  42775  rencldnfilem  43098  cantnfresb  43602  dflim5  43607  ss2iundf  43936  uneqsn  44302  radcnvrat  44591  stoweidlem34  46314  oddneven  47926