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  2660  necon2bd  2954  spcimegf  3551  spcegf  3592  spcimedv  3595  rspcimedv  3613  disjxun  5146  exexneq  5445  sotric  5626  sotrieq  5627  poirr2  6147  dfpo2  6318  funun  6614  imadif  6652  soisoi  7348  onnminsb  7819  oneqmin  7820  ordunisuc2  7865  limsssuc  7871  wfrlem10OLD  8357  tz7.48lem  8480  sdomdif  9164  sdomdomtrfi  9239  domsdomtrfi  9240  pssinf  9290  unblem1  9326  supnub  9500  infnlb  9530  elirrv  9634  inf3lem6  9671  cantnflem1  9727  cardne  10003  cardsdomel  10012  carddom2  10015  cardmin2  10037  alephnbtwn  10109  infdif2  10247  fin4en1  10347  fin23lem31  10381  isf32lem5  10395  isf34lem4  10415  cfpwsdom  10622  fpwwe2  10681  addnidpi  10939  genpnnp  11043  btwnnz  12692  prime  12697  qsqueeze  13240  xralrple  13244  xmullem2  13304  xmulneg1  13308  ssfzoulel  13796  elfznelfzob  13809  bcval4  14343  seqcoll  14500  hashtpg  14521  swrd0  14693  fsumcvg  15745  fsumsplit  15774  fprodcvg  15963  fprodsplit  15999  dvdsle  16344  divalglem8  16434  bitsinv1lem  16475  2mulprm  16727  pockthg  16940  prmunb  16948  vdwlem6  17020  ramlb  17053  gsumzsplit  19960  obselocv  21766  opsrtoslem2  22098  psdmul  22188  elcls  23097  fbasrn  23908  ufilb  23930  ufilmax  23931  rnelfmlem  23976  alexsubALTlem4  24074  tsmssplit  24176  recld2  24850  logbgcd1irr  26852  fsumharmonic  27070  chtub  27271  lgsne0  27394  sltres  27722  nosupbnd2lem1  27775  nocvxminlem  27837  sltlpss  27960  sltmul2  28212  sltonold  28298  axlowdim  28991  wlkp1lem5  29710  wlkp1lem6  29711  cyclnspth  29833  eupth2lem3lem4  30260  cvnsym  32319  cvntr  32321  atcvati  32415  rmounid  32523  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemfrcn0  34511  ballotlemirc  34513  acycgr2v  35135  cusgracyclt3v  35141  fmlasucdisj  35384  nn0prpw  36306  onsucconni  36420  onint1  36432  icorempo  37334  relowlpssretop  37347  fvineqsneq  37395  lindsenlbs  37602  poimirlem16  37623  poimirlem26  37633  fdc  37732  lsatcvat  39032  hlrelat2  39386  ltltncvr  39406  islln2a  39500  islpln2a  39531  islvol2aN  39575  dvrelog2b  42048  rencldnfilem  42808  cantnfresb  43314  dflim5  43319  ss2iundf  43649  uneqsn  44015  radcnvrat  44310  stoweidlem34  45990  oddneven  47569