Theorem con2d 136

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 132	. . 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  137  mt2d  138  pm3.2im  163  exists2  2724  necon2bd  3003  spcimegf  3537  spcegf  3539  spcimedv  3542  rspcimedv  3562  disjxun  5028  sotric  5465  sotrieq  5466  poirr2  5951  funun  6370  imadif  6408  soisoi  7060  onnminsb  7499  oneqmin  7500  ordunisuc2  7539  limsssuc  7545  wfrlem10  7947  tz7.48lem  8060  sdomdif  8649  pssinf  8712  unblem1  8754  supnub  8910  infnlb  8940  elirrv  9044  inf3lem6  9080  cantnflem1  9136  cardne  9378  cardsdomel  9387  carddom2  9390  cardmin2  9412  alephnbtwn  9482  infdif2  9621  fin4en1  9720  fin23lem31  9754  isf32lem5  9768  isf34lem4  9788  cfpwsdom  9995  fpwwe2  10054  addnidpi  10312  genpnnp  10416  btwnnz  12046  prime  12051  qsqueeze  12582  xralrple  12586  xmullem2  12646  xmulneg1  12650  ssfzoulel  13126  elfznelfzob  13138  bcval4  13663  seqcoll  13818  hashtpg  13839  swrd0  14011  fsumcvg  15061  fsumsplit  15089  fprodcvg  15276  fprodsplit  15312  dvdsle  15652  divalglem8  15741  bitsinv1lem  15780  2mulprm  16027  pockthg  16232  prmunb  16240  vdwlem6  16312  ramlb  16345  gsumzsplit  19040  obselocv  20417  opsrtoslem2  20724  elcls  21678  fbasrn  22489  ufilb  22511  ufilmax  22512  rnelfmlem  22557  alexsubALTlem4  22655  tsmssplit  22757  recld2  23419  logbgcd1irr  25380  fsumharmonic  25597  chtub  25796  lgsne0  25919  axlowdim  26755  wlkp1lem5  27467  wlkp1lem6  27468  cyclnspth  27589  eupth2lem3lem4  28016  cvnsym  30073  cvntr  30075  atcvati  30169  rmounid  30266  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemfrcn0  31897  ballotlemirc  31899  acycgr2v  32510  cusgracyclt3v  32516  fmlasucdisj  32759  dfpo2  33104  sltres  33282  nosupbnd2lem1  33328  nocvxminlem  33360  nn0prpw  33784  onsucconni  33898  onint1  33910  icorempo  34768  relowlpssretop  34781  fvineqsneq  34829  lindsenlbs  35052  poimirlem16  35073  poimirlem26  35083  fdc  35183  lsatcvat  36346  hlrelat2  36699  ltltncvr  36719  islln2a  36813  islpln2a  36844  islvol2aN  36888  rencldnfilem  39761  ss2iundf  40360  uneqsn  40726  radcnvrat  41018  stoweidlem34  42676  oddneven  44162