Theorem con2d 132

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 128	. . 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  133  mt2d  134  pm3.2im  159  exists2  2744  exists2OLD  2745  necon2bd  3015  spcimegf  3504  spcegf  3506  spcimedv  3509  rspcimedv  3528  disjxun  4871  sotric  5289  sotrieq  5290  poirr2  5762  funun  6168  imadif  6206  soisoi  6833  onnminsb  7265  oneqmin  7266  ordunisuc2  7305  limsssuc  7311  wfrlem10  7690  tz7.48lem  7802  sdomdif  8377  pssinf  8439  unblem1  8481  supnub  8637  infnlb  8667  elirrv  8770  inf3lem6  8807  cantnflem1  8863  cardne  9104  cardsdomel  9113  carddom2  9116  cardmin2  9137  alephnbtwn  9207  infdif2  9347  fin4en1  9446  fin23lem31  9480  isf32lem5  9494  isf34lem4  9514  cfpwsdom  9721  fpwwe2  9780  addnidpi  10038  genpnnp  10142  btwnnz  11781  prime  11786  qsqueeze  12320  xralrple  12324  xmullem2  12383  xmulneg1  12387  ssfzoulel  12857  elfznelfzob  12869  bcval4  13387  seqcoll  13537  hashtpg  13556  swrd0  13723  fsumcvg  14820  fsumsplit  14848  fprodcvg  15033  fprodsplit  15069  dvdsle  15409  divalglem8  15497  bitsinv1lem  15536  pockthg  15981  prmunb  15989  vdwlem6  16061  ramlb  16094  gsumzsplit  18680  opsrtoslem2  19845  obselocv  20435  elcls  21248  fbasrn  22058  ufilb  22080  ufilmax  22081  rnelfmlem  22126  alexsubALTlem4  22224  tsmssplit  22325  recld2  22987  logbgcd1irr  24934  fsumharmonic  25151  chtub  25350  lgsne0  25473  axlowdim  26260  wlkp1lem5  26978  wlkp1lem6  26979  cyclnspth  27102  eupth2lem3lem4  27608  cvnsym  29704  cvntr  29706  atcvati  29800  ballotlemfc0  31100  ballotlemfcc  31101  ballotlemfrcn0  31137  ballotlemirc  31139  dfpo2  32187  sltres  32354  nosupbnd2lem1  32400  nocvxminlem  32432  nn0prpw  32856  onsucconni  32969  onint1  32981  icorempt2  33744  relowlpssretop  33757  lindsenlbs  33948  poimirlem16  33969  poimirlem26  33979  fdc  34083  lsatcvat  35125  hlrelat2  35478  ltltncvr  35498  islln2a  35592  islpln2a  35623  islvol2aN  35667  rencldnfilem  38228  ss2iundf  38792  uneqsn  39161  radcnvrat  39353  stoweidlem34  41045  oddneven  42387