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  3497  spcegf  3535  spcimedv  3538  rspcimedv  3556  disjxun  5084  exexneq  5388  sotric  5569  sotrieq  5570  poirr2  6088  dfpo2  6261  funun  6545  imadif  6583  soisoi  7283  onnminsb  7753  oneqmin  7754  ordunisuc2  7795  limsssuc  7801  tz7.48lem  8380  sdomdif  9063  sdomdomtrfi  9135  domsdomtrfi  9136  pssinf  9172  unblem1  9202  supnub  9375  infnlb  9406  elirrvOLD  9513  inf3lem6  9554  cantnflem1  9610  cardne  9889  cardsdomel  9898  carddom2  9901  cardmin2  9923  alephnbtwn  9993  infdif2  10131  fin4en1  10231  fin23lem31  10265  isf32lem5  10279  isf34lem4  10299  cfpwsdom  10507  fpwwe2  10566  addnidpi  10824  genpnnp  10928  btwnnz  12605  prime  12610  qsqueeze  13153  xralrple  13157  xmullem2  13217  xmulneg1  13221  ssfzoulel  13715  elfznelfzob  13729  bcval4  14269  seqcoll  14426  hashtpg  14447  swrd0  14621  fsumcvg  15674  fsumsplit  15703  fprodcvg  15895  fprodsplit  15931  dvdsle  16279  divalglem8  16369  bitsinv1lem  16410  2mulprm  16662  pockthg  16877  prmunb  16885  vdwlem6  16957  ramlb  16990  chnpof1  18596  gsumzsplit  19902  obselocv  21708  opsrtoslem2  22034  psdmul  22132  elcls  23038  fbasrn  23849  ufilb  23871  ufilmax  23872  rnelfmlem  23917  alexsubALTlem4  24015  tsmssplit  24117  recld2  24780  logbgcd1irr  26758  fsumharmonic  26975  chtub  27175  lgsne0  27298  ltsres  27626  nosupbnd2lem1  27679  nocvxminlem  27746  ltslpss  27900  ltmuls2  28163  ltonold  28253  axlowdim  29030  wlkp1lem5  29744  wlkp1lem6  29745  cyclnspth  29869  eupth2lem3lem4  30301  cvnsym  32361  cvntr  32363  atcvati  32457  rmounid  32564  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemfrcn0  34674  ballotlemirc  34676  acycgr2v  35332  cusgracyclt3v  35338  fmlasucdisj  35581  nn0prpw  36505  onsucconni  36619  onint1  36631  icorempo  37667  relowlpssretop  37680  fvineqsneq  37728  lindsenlbs  37936  poimirlem16  37957  poimirlem26  37967  fdc  38066  lsatcvat  39496  hlrelat2  39849  ltltncvr  39869  islln2a  39963  islpln2a  39994  islvol2aN  40038  dvrelog2b  42505  mullt0b2d  42929  rencldnfilem  43248  cantnfresb  43752  dflim5  43757  ss2iundf  44086  uneqsn  44452  radcnvrat  44741  stoweidlem34  46462  oddneven  48114