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  3517  spcegf  3549  spcimedv  3552  rspcimedv  3570  disjxun  5105  exexneq  5414  sotric  5597  sotrieq  5598  poirr2  6122  dfpo2  6298  funun  6583  imadif  6621  soisoi  7332  onnminsb  7801  oneqmin  7802  ordunisuc2  7843  limsssuc  7849  tz7.48lem  8433  sdomdif  9126  sdomdomtrfi  9198  domsdomtrfi  9199  pssinf  9235  unblem1  9265  supnub  9435  infnlb  9466  elirrv  9572  elirrvOLDOLD  9574  inf3lem6  9615  cantnflem1  9671  cardne  9973  cardsdomel  9982  carddom2  9985  cardmin2  10007  alephnbtwn  10077  infdif2  10214  fin4en1  10314  fin23lem31  10348  isf32lem5  10362  isf34lem4  10382  cfpwsdom  10596  fpwwe2  10655  addnidpi  10913  genpnnp  11017  btwnnz  12700  prime  12705  qsqueeze  13255  xralrple  13259  xmullem2  13319  xmulneg1  13323  ssfzoulel  13818  elfznelfzob  13832  bcval4  14373  seqcoll  14531  hashtpg  14552  swrd0  14730  fsumcvg  15800  fsumsplit  15829  fprodcvg  16021  fprodsplit  16057  dvdsle  16404  divalglem8  16494  bitsinv1lem  16535  2mulprm  16787  pockthg  17002  prmunb  17010  vdwlem6  17082  ramlb  17115  chnpof1  18722  gsumzsplit  20058  obselocv  21945  lindsenlbs  22068  opsrtoslem2  22276  psdmul  22398  elcls  23302  fbasrn  24114  ufilb  24136  ufilmax  24137  rnelfmlem  24182  alexsubALTlem4  24280  tsmssplit  24382  recld2  25045  logbgcd1irr  27032  fsumharmonic  27249  chtub  27449  lgsne0  27572  ltsres  27899  nosupbnd2lem1  27952  nocvxminlem  28020  ltslpss  28174  ltmuls2  28437  ltonold  28527  axlowdim  29419  wlkp1lem5  30136  wlkp1lem6  30137  cyclnspth  30269  eupth2lem3lem4  30712  cvnsym  32772  cvntr  32774  atcvati  32868  rmounid  32971  ballotlemfc0  35006  ballotlemfcc  35007  ballotlemfrcn0  35043  ballotlemirc  35045  acycgr2v  35731  cusgracyclt3v  35737  fmlasucdisj  35980  nmulprop  36772  nn0prpw  36944  onsucconni  37058  onint1  37070  icorempo  38107  relowlpssretop  38120  fvineqsneq  38168  poimirlem16  38387  poimirlem26  38397  fdc  38497  lsatcvat  39925  hlrelat2  40278  ltltncvr  40298  islln2a  40392  islpln2a  40423  islvol2aN  40467  dvrelog2b  42934  mullt0b2d  43374  rencldnfilem  43663  cantnfresb  44167  dflim5  44172  ss2iundf  44501  uneqsn  44867  radcnvrat  45140  stoweidlem34  46864  oddneven  48562