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  2665  necon2bd  2962  spcimegf  3563  spcegf  3605  spcimedv  3608  rspcimedv  3626  disjxun  5164  exexneq  5454  sotric  5637  sotrieq  5638  poirr2  6156  dfpo2  6327  funun  6624  imadif  6662  soisoi  7364  onnminsb  7835  oneqmin  7836  ordunisuc2  7881  limsssuc  7887  wfrlem10OLD  8374  tz7.48lem  8497  sdomdif  9191  sdomdomtrfi  9267  domsdomtrfi  9268  pssinf  9319  unblem1  9356  supnub  9531  infnlb  9561  elirrv  9665  inf3lem6  9702  cantnflem1  9758  cardne  10034  cardsdomel  10043  carddom2  10046  cardmin2  10068  alephnbtwn  10140  infdif2  10278  fin4en1  10378  fin23lem31  10412  isf32lem5  10426  isf34lem4  10446  cfpwsdom  10653  fpwwe2  10712  addnidpi  10970  genpnnp  11074  btwnnz  12719  prime  12724  qsqueeze  13263  xralrple  13267  xmullem2  13327  xmulneg1  13331  ssfzoulel  13810  elfznelfzob  13823  bcval4  14356  seqcoll  14513  hashtpg  14534  swrd0  14706  fsumcvg  15760  fsumsplit  15789  fprodcvg  15978  fprodsplit  16014  dvdsle  16358  divalglem8  16448  bitsinv1lem  16487  2mulprm  16740  pockthg  16953  prmunb  16961  vdwlem6  17033  ramlb  17066  gsumzsplit  19969  obselocv  21771  opsrtoslem2  22103  psdmul  22193  elcls  23102  fbasrn  23913  ufilb  23935  ufilmax  23936  rnelfmlem  23981  alexsubALTlem4  24079  tsmssplit  24181  recld2  24855  logbgcd1irr  26855  fsumharmonic  27073  chtub  27274  lgsne0  27397  sltres  27725  nosupbnd2lem1  27778  nocvxminlem  27840  sltlpss  27963  sltmul2  28215  sltonold  28301  axlowdim  28994  wlkp1lem5  29713  wlkp1lem6  29714  cyclnspth  29836  eupth2lem3lem4  30263  cvnsym  32322  cvntr  32324  atcvati  32418  rmounid  32523  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemfrcn0  34494  ballotlemirc  34496  acycgr2v  35118  cusgracyclt3v  35124  fmlasucdisj  35367  nn0prpw  36289  onsucconni  36403  onint1  36415  icorempo  37317  relowlpssretop  37330  fvineqsneq  37378  lindsenlbs  37575  poimirlem16  37596  poimirlem26  37606  fdc  37705  lsatcvat  39006  hlrelat2  39360  ltltncvr  39380  islln2a  39474  islpln2a  39505  islvol2aN  39549  dvrelog2b  42023  rencldnfilem  42776  cantnfresb  43286  dflim5  43291  ss2iundf  43621  uneqsn  43987  radcnvrat  44283  stoweidlem34  45955  oddneven  47518