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  2658  necon2bd  2957  spcimegf  3581  spcegf  3583  spcimedv  3586  rspcimedv  3604  disjxun  5146  exexneq  5434  sotric  5616  sotrieq  5617  poirr2  6123  dfpo2  6293  funun  6592  imadif  6630  soisoi  7322  onnminsb  7784  oneqmin  7785  ordunisuc2  7830  limsssuc  7836  wfrlem10OLD  8315  tz7.48lem  8438  sdomdif  9122  sdomdomtrfi  9201  domsdomtrfi  9202  pssinf  9253  unblem1  9292  supnub  9454  infnlb  9484  elirrv  9588  inf3lem6  9625  cantnflem1  9681  cardne  9957  cardsdomel  9966  carddom2  9969  cardmin2  9991  alephnbtwn  10063  infdif2  10202  fin4en1  10301  fin23lem31  10335  isf32lem5  10349  isf34lem4  10369  cfpwsdom  10576  fpwwe2  10635  addnidpi  10893  genpnnp  10997  btwnnz  12635  prime  12640  qsqueeze  13177  xralrple  13181  xmullem2  13241  xmulneg1  13245  ssfzoulel  13723  elfznelfzob  13735  bcval4  14264  seqcoll  14422  hashtpg  14443  swrd0  14605  fsumcvg  15655  fsumsplit  15684  fprodcvg  15871  fprodsplit  15907  dvdsle  16250  divalglem8  16340  bitsinv1lem  16379  2mulprm  16627  pockthg  16836  prmunb  16844  vdwlem6  16916  ramlb  16949  gsumzsplit  19790  obselocv  21275  opsrtoslem2  21609  elcls  22569  fbasrn  23380  ufilb  23402  ufilmax  23403  rnelfmlem  23448  alexsubALTlem4  23546  tsmssplit  23648  recld2  24322  logbgcd1irr  26289  fsumharmonic  26506  chtub  26705  lgsne0  26828  sltres  27155  nosupbnd2lem1  27208  nocvxminlem  27269  sltlpss  27391  sltmul2  27613  axlowdim  28209  wlkp1lem5  28924  wlkp1lem6  28925  cyclnspth  29047  eupth2lem3lem4  29474  cvnsym  31531  cvntr  31533  atcvati  31627  rmounid  31723  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemfrcn0  33517  ballotlemirc  33519  acycgr2v  34130  cusgracyclt3v  34136  fmlasucdisj  34379  nn0prpw  35197  onsucconni  35311  onint1  35323  icorempo  36221  relowlpssretop  36234  fvineqsneq  36282  lindsenlbs  36472  poimirlem16  36493  poimirlem26  36503  fdc  36602  lsatcvat  37909  hlrelat2  38263  ltltncvr  38283  islln2a  38377  islpln2a  38408  islvol2aN  38452  dvrelog2b  40920  rencldnfilem  41544  cantnfresb  42060  dflim5  42065  ss2iundf  42396  uneqsn  42762  radcnvrat  43059  stoweidlem34  44737  oddneven  46299