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  2655  necon2bd  2941  spcimegf  3508  spcegf  3549  spcimedv  3552  rspcimedv  3570  disjxun  5093  exexneq  5381  sotric  5561  sotrieq  5562  poirr2  6077  dfpo2  6248  funun  6532  imadif  6570  soisoi  7269  onnminsb  7739  oneqmin  7740  ordunisuc2  7784  limsssuc  7790  tz7.48lem  8370  sdomdif  9049  sdomdomtrfi  9125  domsdomtrfi  9126  pssinf  9161  unblem1  9197  supnub  9371  infnlb  9402  elirrvOLD  9509  inf3lem6  9548  cantnflem1  9604  cardne  9880  cardsdomel  9889  carddom2  9892  cardmin2  9914  alephnbtwn  9984  infdif2  10122  fin4en1  10222  fin23lem31  10256  isf32lem5  10270  isf34lem4  10290  cfpwsdom  10497  fpwwe2  10556  addnidpi  10814  genpnnp  10918  btwnnz  12570  prime  12575  qsqueeze  13121  xralrple  13125  xmullem2  13185  xmulneg1  13189  ssfzoulel  13681  elfznelfzob  13694  bcval4  14232  seqcoll  14389  hashtpg  14410  swrd0  14583  fsumcvg  15637  fsumsplit  15666  fprodcvg  15855  fprodsplit  15891  dvdsle  16239  divalglem8  16329  bitsinv1lem  16370  2mulprm  16622  pockthg  16836  prmunb  16844  vdwlem6  16916  ramlb  16949  gsumzsplit  19824  obselocv  21653  opsrtoslem2  21979  psdmul  22069  elcls  22976  fbasrn  23787  ufilb  23809  ufilmax  23810  rnelfmlem  23855  alexsubALTlem4  23953  tsmssplit  24055  recld2  24719  logbgcd1irr  26720  fsumharmonic  26938  chtub  27139  lgsne0  27262  sltres  27590  nosupbnd2lem1  27643  nocvxminlem  27706  sltlpss  27840  sltmul2  28097  sltonold  28185  axlowdim  28924  wlkp1lem5  29639  wlkp1lem6  29640  cyclnspth  29764  eupth2lem3lem4  30193  cvnsym  32252  cvntr  32254  atcvati  32348  rmounid  32457  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemfrcn0  34497  ballotlemirc  34499  acycgr2v  35122  cusgracyclt3v  35128  fmlasucdisj  35371  nn0prpw  36296  onsucconni  36410  onint1  36422  icorempo  37324  relowlpssretop  37337  fvineqsneq  37385  lindsenlbs  37594  poimirlem16  37615  poimirlem26  37625  fdc  37724  lsatcvat  39028  hlrelat2  39382  ltltncvr  39402  islln2a  39496  islpln2a  39527  islvol2aN  39571  dvrelog2b  42039  mullt0b2d  42457  rencldnfilem  42793  cantnfresb  43297  dflim5  43302  ss2iundf  43632  uneqsn  43998  radcnvrat  44287  stoweidlem34  46016  oddneven  47629