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  2656  necon2bd  2942  spcimegf  3520  spcegf  3561  spcimedv  3564  rspcimedv  3582  disjxun  5108  exexneq  5397  sotric  5579  sotrieq  5580  poirr2  6100  dfpo2  6272  funun  6565  imadif  6603  soisoi  7306  onnminsb  7778  oneqmin  7779  ordunisuc2  7823  limsssuc  7829  tz7.48lem  8412  sdomdif  9095  sdomdomtrfi  9171  domsdomtrfi  9172  pssinf  9210  unblem1  9246  supnub  9420  infnlb  9451  elirrv  9556  inf3lem6  9593  cantnflem1  9649  cardne  9925  cardsdomel  9934  carddom2  9937  cardmin2  9959  alephnbtwn  10031  infdif2  10169  fin4en1  10269  fin23lem31  10303  isf32lem5  10317  isf34lem4  10337  cfpwsdom  10544  fpwwe2  10603  addnidpi  10861  genpnnp  10965  btwnnz  12617  prime  12622  qsqueeze  13168  xralrple  13172  xmullem2  13232  xmulneg1  13236  ssfzoulel  13728  elfznelfzob  13741  bcval4  14279  seqcoll  14436  hashtpg  14457  swrd0  14630  fsumcvg  15685  fsumsplit  15714  fprodcvg  15903  fprodsplit  15939  dvdsle  16287  divalglem8  16377  bitsinv1lem  16418  2mulprm  16670  pockthg  16884  prmunb  16892  vdwlem6  16964  ramlb  16997  gsumzsplit  19864  obselocv  21644  opsrtoslem2  21970  psdmul  22060  elcls  22967  fbasrn  23778  ufilb  23800  ufilmax  23801  rnelfmlem  23846  alexsubALTlem4  23944  tsmssplit  24046  recld2  24710  logbgcd1irr  26711  fsumharmonic  26929  chtub  27130  lgsne0  27253  sltres  27581  nosupbnd2lem1  27634  nocvxminlem  27696  sltlpss  27826  sltmul2  28081  sltonold  28169  axlowdim  28895  wlkp1lem5  29612  wlkp1lem6  29613  cyclnspth  29738  eupth2lem3lem4  30167  cvnsym  32226  cvntr  32228  atcvati  32322  rmounid  32431  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemfrcn0  34528  ballotlemirc  34530  acycgr2v  35144  cusgracyclt3v  35150  fmlasucdisj  35393  nn0prpw  36318  onsucconni  36432  onint1  36444  icorempo  37346  relowlpssretop  37359  fvineqsneq  37407  lindsenlbs  37616  poimirlem16  37637  poimirlem26  37647  fdc  37746  lsatcvat  39050  hlrelat2  39404  ltltncvr  39424  islln2a  39518  islpln2a  39549  islvol2aN  39593  dvrelog2b  42061  mullt0b2d  42479  rencldnfilem  42815  cantnfresb  43320  dflim5  43325  ss2iundf  43655  uneqsn  44021  radcnvrat  44310  stoweidlem34  46039  oddneven  47649