Theorem con2d 135

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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 116	1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con2  136  mt2d  137  pm3.2im  161  exists2  2688  necon2bd  2973  spcimegf  3518  spcegf  3550  spcimedv  3553  rspcimedv  3571  disjxun  5106  exexneq  5415  sotric  5598  sotrieq  5599  poirr2  6123  dfpo2  6297  funun  6582  imadif  6620  soisoi  7326  onnminsb  7796  oneqmin  7797  ordunisuc2  7838  limsssuc  7844  tz7.48lem  8426  sdomdif  9111  sdomdomtrfi  9183  domsdomtrfi  9184  pssinf  9220  unblem1  9250  supnub  9420  infnlb  9451  elirrv  9557  elirrvOLDOLD  9559  inf3lem6  9600  cantnflem1  9656  cardne  9958  cardsdomel  9967  carddom2  9970  cardmin2  9992  alephnbtwn  10062  infdif2  10199  fin4en1  10299  fin23lem31  10333  isf32lem5  10347  isf34lem4  10367  cfpwsdom  10575  fpwwe2  10634  addnidpi  10892  genpnnp  10996  btwnnz  12678  prime  12683  qsqueeze  13233  xralrple  13237  xmullem2  13297  xmulneg1  13301  ssfzoulel  13796  elfznelfzob  13810  bcval4  14350  seqcoll  14508  hashtpg  14529  swrd0  14703  fsumcvg  15770  fsumsplit  15799  fprodcvg  15991  fprodsplit  16027  dvdsle  16374  divalglem8  16464  bitsinv1lem  16505  2mulprm  16757  pockthg  16972  prmunb  16980  vdwlem6  17052  ramlb  17085  chnpof1  18692  gsumzsplit  20003  obselocv  21889  opsrtoslem2  22218  psdmul  22340  elcls  23241  fbasrn  24052  ufilb  24074  ufilmax  24075  rnelfmlem  24120  alexsubALTlem4  24218  tsmssplit  24320  recld2  24983  logbgcd1irr  26970  fsumharmonic  27187  chtub  27387  lgsne0  27510  ltsres  27837  nosupbnd2lem1  27890  nocvxminlem  27958  ltslpss  28112  ltmuls2  28375  ltonold  28465  axlowdim  29322  wlkp1lem5  30036  wlkp1lem6  30037  cyclnspth  30161  eupth2lem3lem4  30593  cvnsym  32653  cvntr  32655  atcvati  32749  rmounid  32852  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemfrcn0  34929  ballotlemirc  34931  acycgr2v  35650  cusgracyclt3v  35656  fmlasucdisj  35899  nmulprop  36690  nn0prpw  36862  onsucconni  36976  onint1  36988  icorempo  38025  relowlpssretop  38038  fvineqsneq  38086  lindsenlbs  38294  poimirlem16  38315  poimirlem26  38325  fdc  38424  lsatcvat  39852  hlrelat2  40205  ltltncvr  40225  islln2a  40319  islpln2a  40350  islvol2aN  40394  dvrelog2b  42861  mullt0b2d  43286  rencldnfilem  43575  cantnfresb  44079  dflim5  44084  ss2iundf  44413  uneqsn  44779  radcnvrat  45052  stoweidlem34  46776  oddneven  48437