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  2682  necon2bd  2967  spcimegf  3513  spcegf  3546  spcimedv  3549  rspcimedv  3567  disjxun  5092  exexneq  5396  sotric  5578  sotrieq  5579  poirr2  6101  dfpo2  6272  funun  6556  imadif  6594  soisoi  7301  onnminsb  7771  oneqmin  7772  ordunisuc2  7813  limsssuc  7819  tz7.48lem  8400  sdomdif  9086  sdomdomtrfi  9158  domsdomtrfi  9159  pssinf  9195  unblem1  9225  supnub  9398  infnlb  9429  elirrv  9535  elirrvOLDOLD  9537  inf3lem6  9578  cantnflem1  9634  cardne  9913  cardsdomel  9922  carddom2  9925  cardmin2  9947  alephnbtwn  10017  infdif2  10155  fin4en1  10256  fin23lem31  10290  isf32lem5  10304  isf34lem4  10324  cfpwsdom  10532  fpwwe2  10591  addnidpi  10849  genpnnp  10953  btwnnz  12639  prime  12644  qsqueeze  13194  xralrple  13198  xmullem2  13258  xmulneg1  13262  ssfzoulel  13756  elfznelfzob  13770  bcval4  14310  seqcoll  14467  hashtpg  14488  swrd0  14662  fsumcvg  15715  fsumsplit  15744  fprodcvg  15936  fprodsplit  15972  dvdsle  16320  divalglem8  16410  bitsinv1lem  16451  2mulprm  16703  pockthg  16918  prmunb  16926  vdwlem6  16998  ramlb  17031  chnpof1  18638  gsumzsplit  19943  obselocv  21753  opsrtoslem2  22082  psdmul  22204  elcls  23106  fbasrn  23917  ufilb  23939  ufilmax  23940  rnelfmlem  23985  alexsubALTlem4  24083  tsmssplit  24185  recld2  24848  logbgcd1irr  26829  fsumharmonic  27046  chtub  27246  lgsne0  27369  ltsres  27696  nosupbnd2lem1  27749  nocvxminlem  27817  ltslpss  27971  ltmuls2  28234  ltonold  28324  axlowdim  29101  wlkp1lem5  29815  wlkp1lem6  29816  cyclnspth  29940  eupth2lem3lem4  30372  cvnsym  32432  cvntr  32434  atcvati  32528  rmounid  32635  ballotlemfc0  34744  ballotlemfcc  34745  ballotlemfrcn0  34781  ballotlemirc  34783  acycgr2v  35448  cusgracyclt3v  35454  fmlasucdisj  35697  nmulprop  36488  nn0prpw  36631  onsucconni  36745  onint1  36757  icorempo  37793  relowlpssretop  37806  fvineqsneq  37854  lindsenlbs  38062  poimirlem16  38083  poimirlem26  38093  fdc  38192  lsatcvat  39622  hlrelat2  39975  ltltncvr  39995  islln2a  40089  islpln2a  40120  islvol2aN  40164  dvrelog2b  42631  mullt0b2d  43054  rencldnfilem  43345  cantnfresb  43849  dflim5  43854  ss2iundf  44183  uneqsn  44549  radcnvrat  44838  stoweidlem34  46556  oddneven  48214