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  5147  exexneq  5435  sotric  5617  sotrieq  5618  poirr2  6126  dfpo2  6296  funun  6595  imadif  6633  soisoi  7325  onnminsb  7787  oneqmin  7788  ordunisuc2  7833  limsssuc  7839  wfrlem10OLD  8318  tz7.48lem  8441  sdomdif  9125  sdomdomtrfi  9204  domsdomtrfi  9205  pssinf  9256  unblem1  9295  supnub  9457  infnlb  9487  elirrv  9591  inf3lem6  9628  cantnflem1  9684  cardne  9960  cardsdomel  9969  carddom2  9972  cardmin2  9994  alephnbtwn  10066  infdif2  10205  fin4en1  10304  fin23lem31  10338  isf32lem5  10352  isf34lem4  10372  cfpwsdom  10579  fpwwe2  10638  addnidpi  10896  genpnnp  11000  btwnnz  12638  prime  12643  qsqueeze  13180  xralrple  13184  xmullem2  13244  xmulneg1  13248  ssfzoulel  13726  elfznelfzob  13738  bcval4  14267  seqcoll  14425  hashtpg  14446  swrd0  14608  fsumcvg  15658  fsumsplit  15687  fprodcvg  15874  fprodsplit  15910  dvdsle  16253  divalglem8  16343  bitsinv1lem  16382  2mulprm  16630  pockthg  16839  prmunb  16847  vdwlem6  16919  ramlb  16952  gsumzsplit  19795  obselocv  21283  opsrtoslem2  21617  elcls  22577  fbasrn  23388  ufilb  23410  ufilmax  23411  rnelfmlem  23456  alexsubALTlem4  23554  tsmssplit  23656  recld2  24330  logbgcd1irr  26299  fsumharmonic  26516  chtub  26715  lgsne0  26838  sltres  27165  nosupbnd2lem1  27218  nocvxminlem  27279  sltlpss  27402  sltmul2  27626  sltonold  27690  axlowdim  28250  wlkp1lem5  28965  wlkp1lem6  28966  cyclnspth  29088  eupth2lem3lem4  29515  cvnsym  31574  cvntr  31576  atcvati  31670  rmounid  31766  ballotlemfc0  33522  ballotlemfcc  33523  ballotlemfrcn0  33559  ballotlemirc  33561  acycgr2v  34172  cusgracyclt3v  34178  fmlasucdisj  34421  nn0prpw  35256  onsucconni  35370  onint1  35382  icorempo  36280  relowlpssretop  36293  fvineqsneq  36341  lindsenlbs  36531  poimirlem16  36552  poimirlem26  36562  fdc  36661  lsatcvat  37968  hlrelat2  38322  ltltncvr  38342  islln2a  38436  islpln2a  38467  islvol2aN  38511  dvrelog2b  40979  rencldnfilem  41606  cantnfresb  42122  dflim5  42127  ss2iundf  42458  uneqsn  42824  radcnvrat  43121  stoweidlem34  44798  oddneven  46360