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  2662  necon2bd  2949  spcimegf  3535  spcegf  3576  spcimedv  3579  rspcimedv  3597  disjxun  5122  exexneq  5414  sotric  5596  sotrieq  5597  poirr2  6118  dfpo2  6290  funun  6587  imadif  6625  soisoi  7326  onnminsb  7798  oneqmin  7799  ordunisuc2  7844  limsssuc  7850  wfrlem10OLD  8337  tz7.48lem  8460  sdomdif  9144  sdomdomtrfi  9220  domsdomtrfi  9221  pssinf  9269  unblem1  9305  supnub  9479  infnlb  9510  elirrv  9615  inf3lem6  9652  cantnflem1  9708  cardne  9984  cardsdomel  9993  carddom2  9996  cardmin2  10018  alephnbtwn  10090  infdif2  10228  fin4en1  10328  fin23lem31  10362  isf32lem5  10376  isf34lem4  10396  cfpwsdom  10603  fpwwe2  10662  addnidpi  10920  genpnnp  11024  btwnnz  12674  prime  12679  qsqueeze  13222  xralrple  13226  xmullem2  13286  xmulneg1  13290  ssfzoulel  13781  elfznelfzob  13794  bcval4  14330  seqcoll  14487  hashtpg  14508  swrd0  14681  fsumcvg  15733  fsumsplit  15762  fprodcvg  15951  fprodsplit  15987  dvdsle  16334  divalglem8  16424  bitsinv1lem  16465  2mulprm  16717  pockthg  16931  prmunb  16939  vdwlem6  17011  ramlb  17044  gsumzsplit  19913  obselocv  21693  opsrtoslem2  22019  psdmul  22109  elcls  23016  fbasrn  23827  ufilb  23849  ufilmax  23850  rnelfmlem  23895  alexsubALTlem4  23993  tsmssplit  24095  recld2  24759  logbgcd1irr  26761  fsumharmonic  26979  chtub  27180  lgsne0  27303  sltres  27631  nosupbnd2lem1  27684  nocvxminlem  27746  sltlpss  27876  sltmul2  28131  sltonold  28219  axlowdim  28945  wlkp1lem5  29662  wlkp1lem6  29663  cyclnspth  29788  eupth2lem3lem4  30217  cvnsym  32276  cvntr  32278  atcvati  32372  rmounid  32481  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemfrcn0  34567  ballotlemirc  34569  acycgr2v  35177  cusgracyclt3v  35183  fmlasucdisj  35426  nn0prpw  36346  onsucconni  36460  onint1  36472  icorempo  37374  relowlpssretop  37387  fvineqsneq  37435  lindsenlbs  37644  poimirlem16  37665  poimirlem26  37675  fdc  37774  lsatcvat  39073  hlrelat2  39427  ltltncvr  39447  islln2a  39541  islpln2a  39572  islvol2aN  39616  dvrelog2b  42084  rencldnfilem  42818  cantnfresb  43323  dflim5  43328  ss2iundf  43658  uneqsn  44024  radcnvrat  44313  stoweidlem34  46043  oddneven  47638