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  2666  necon2bd  2951  spcimegf  3499  spcegf  3537  spcimedv  3540  rspcimedv  3558  disjxun  5077  exexneq  5381  sotric  5563  sotrieq  5564  poirr2  6081  dfpo2  6254  funun  6538  imadif  6576  soisoi  7279  onnminsb  7749  oneqmin  7750  ordunisuc2  7791  limsssuc  7797  tz7.48lem  8377  sdomdif  9060  sdomdomtrfi  9132  domsdomtrfi  9133  pssinf  9169  unblem1  9199  supnub  9372  infnlb  9403  elirrv  9509  elirrvOLDOLD  9511  inf3lem6  9552  cantnflem1  9608  cardne  9887  cardsdomel  9896  carddom2  9899  cardmin2  9921  alephnbtwn  9991  infdif2  10129  fin4en1  10229  fin23lem31  10263  isf32lem5  10277  isf34lem4  10297  cfpwsdom  10505  fpwwe2  10564  addnidpi  10822  genpnnp  10926  btwnnz  12603  prime  12608  qsqueeze  13151  xralrple  13155  xmullem2  13215  xmulneg1  13219  ssfzoulel  13713  elfznelfzob  13727  bcval4  14267  seqcoll  14424  hashtpg  14445  swrd0  14619  fsumcvg  15672  fsumsplit  15701  fprodcvg  15893  fprodsplit  15929  dvdsle  16277  divalglem8  16367  bitsinv1lem  16408  2mulprm  16660  pockthg  16875  prmunb  16883  vdwlem6  16955  ramlb  16988  chnpof1  18594  gsumzsplit  19900  obselocv  21710  opsrtoslem2  22039  psdmul  22161  elcls  23063  fbasrn  23874  ufilb  23896  ufilmax  23897  rnelfmlem  23942  alexsubALTlem4  24040  tsmssplit  24142  recld2  24805  logbgcd1irr  26783  fsumharmonic  27000  chtub  27200  lgsne0  27323  ltsres  27651  nosupbnd2lem1  27704  nocvxminlem  27771  ltslpss  27925  ltmuls2  28188  ltonold  28278  axlowdim  29055  wlkp1lem5  29769  wlkp1lem6  29770  cyclnspth  29894  eupth2lem3lem4  30326  cvnsym  32386  cvntr  32388  atcvati  32482  rmounid  32589  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemfrcn0  34721  ballotlemirc  34723  acycgr2v  35379  cusgracyclt3v  35385  fmlasucdisj  35628  nn0prpw  36552  onsucconni  36666  onint1  36678  icorempo  37714  relowlpssretop  37727  fvineqsneq  37775  lindsenlbs  37983  poimirlem16  38004  poimirlem26  38014  fdc  38113  lsatcvat  39543  hlrelat2  39896  ltltncvr  39916  islln2a  40010  islpln2a  40041  islvol2aN  40085  dvrelog2b  42552  mullt0b2d  42975  rencldnfilem  43266  cantnfresb  43770  dflim5  43775  ss2iundf  44104  uneqsn  44470  radcnvrat  44759  stoweidlem34  46478  oddneven  48136