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  2649  necon2bd  2948  spcimegf  3572  spcegf  3574  spcimedv  3577  rspcimedv  3595  disjxun  5136  exexneq  5424  sotric  5606  sotrieq  5607  poirr2  6115  dfpo2  6285  funun  6584  imadif  6622  soisoi  7317  onnminsb  7780  oneqmin  7781  ordunisuc2  7826  limsssuc  7832  wfrlem10OLD  8313  tz7.48lem  8436  sdomdif  9120  sdomdomtrfi  9199  domsdomtrfi  9200  pssinf  9251  unblem1  9290  supnub  9452  infnlb  9482  elirrv  9586  inf3lem6  9623  cantnflem1  9679  cardne  9955  cardsdomel  9964  carddom2  9967  cardmin2  9989  alephnbtwn  10061  infdif2  10200  fin4en1  10299  fin23lem31  10333  isf32lem5  10347  isf34lem4  10367  cfpwsdom  10574  fpwwe2  10633  addnidpi  10891  genpnnp  10995  btwnnz  12634  prime  12639  qsqueeze  13176  xralrple  13180  xmullem2  13240  xmulneg1  13244  ssfzoulel  13722  elfznelfzob  13734  bcval4  14263  seqcoll  14421  hashtpg  14442  swrd0  14604  fsumcvg  15654  fsumsplit  15683  fprodcvg  15870  fprodsplit  15906  dvdsle  16249  divalglem8  16339  bitsinv1lem  16378  2mulprm  16626  pockthg  16837  prmunb  16845  vdwlem6  16917  ramlb  16950  gsumzsplit  19836  obselocv  21590  opsrtoslem2  21926  elcls  22898  fbasrn  23709  ufilb  23731  ufilmax  23732  rnelfmlem  23777  alexsubALTlem4  23875  tsmssplit  23977  recld2  24651  logbgcd1irr  26641  fsumharmonic  26859  chtub  27060  lgsne0  27183  sltres  27510  nosupbnd2lem1  27563  nocvxminlem  27625  sltlpss  27748  sltmul2  27986  sltonold  28068  axlowdim  28654  wlkp1lem5  29369  wlkp1lem6  29370  cyclnspth  29492  eupth2lem3lem4  29919  cvnsym  31978  cvntr  31980  atcvati  32074  rmounid  32170  ballotlemfc0  33946  ballotlemfcc  33947  ballotlemfrcn0  33983  ballotlemirc  33985  acycgr2v  34596  cusgracyclt3v  34602  fmlasucdisj  34845  nn0prpw  35664  onsucconni  35778  onint1  35790  icorempo  36688  relowlpssretop  36701  fvineqsneq  36749  lindsenlbs  36939  poimirlem16  36960  poimirlem26  36970  fdc  37069  lsatcvat  38376  hlrelat2  38730  ltltncvr  38750  islln2a  38844  islpln2a  38875  islvol2aN  38919  dvrelog2b  41390  rencldnfilem  42013  cantnfresb  42529  dflim5  42534  ss2iundf  42865  uneqsn  43231  radcnvrat  43528  stoweidlem34  45201  oddneven  46763