Theorem con2d 129

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 125	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 114	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  130  mt2d  131  pm3.2im  157  exists2  2562  necon2bd  2810  spcimegf  3287  spcegf  3289  spcimedv  3292  rspcimedv  3311  minelOLD  4034  disjxun  4651  sotric  5061  sotrieq  5062  poirr2  5520  funun  5932  imadif  5973  soisoi  6578  onnminsb  7004  oneqmin  7005  ordunisuc2  7044  limsssuc  7050  wfrlem10  7424  tz7.48lem  7536  sdomdif  8108  pssinf  8170  unblem1  8212  supnub  8368  infnlb  8398  elirrv  8504  inf3lem6  8530  cantnflem1  8586  cardne  8791  cardsdomel  8800  carddom2  8803  cardmin2  8824  alephnbtwn  8894  infdif2  9032  fin4en1  9131  fin23lem31  9165  isf32lem5  9179  isf34lem4  9199  cfpwsdom  9406  fpwwe2  9465  addnidpi  9723  genpnnp  9827  btwnnz  11453  prime  11458  qsqueeze  12032  xralrple  12036  xmullem2  12095  xmulneg1  12099  ssfzoulel  12562  elfznelfzob  12574  bcval4  13094  seqcoll  13248  hashtpg  13267  swrd0  13434  fsumcvg  14443  fsumsplit  14471  fprodcvg  14660  fprodsplit  14696  dvdsle  15032  divalglem8  15123  bitsinv1lem  15163  pockthg  15610  prmunb  15618  vdwlem6  15690  ramlb  15723  gsumzsplit  18327  opsrtoslem2  19485  obselocv  20072  elcls  20877  fbasrn  21688  ufilb  21710  ufilmax  21711  rnelfmlem  21756  alexsubALTlem4  21854  tsmssplit  21955  recld2  22617  fsumharmonic  24738  chtub  24937  lgsne0  25060  axlowdim  25841  nbgrssovtx  26260  wlkp1lem5  26574  wlkp1lem6  26575  cyclnspth  26695  eupth2lem3lem4  27091  cvnsym  29149  cvntr  29151  atcvati  29245  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemfrcn0  30591  ballotlemirc  30593  dfpo2  31645  sltres  31815  nosupbnd2lem1  31861  nocvxminlem  31893  nn0prpw  32318  onsucconni  32436  onint1  32448  icorempt2  33199  relowlpssretop  33212  lindsenlbs  33404  poimirlem16  33425  poimirlem26  33435  fdc  33541  lsatcvat  34337  hlrelat2  34689  ltltncvr  34709  islln2a  34803  islpln2a  34834  islvol2aN  34878  rencldnfilem  37384  ss2iundf  37951  uneqsn  38321  radcnvrat  38513  stoweidlem34  40251  oddneven  41557