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  3517  spcegf  3558  spcimedv  3561  rspcimedv  3579  disjxun  5105  exexneq  5394  sotric  5576  sotrieq  5577  poirr2  6097  dfpo2  6269  funun  6562  imadif  6600  soisoi  7303  onnminsb  7775  oneqmin  7776  ordunisuc2  7820  limsssuc  7826  tz7.48lem  8409  sdomdif  9089  sdomdomtrfi  9165  domsdomtrfi  9166  pssinf  9203  unblem1  9239  supnub  9413  infnlb  9444  elirrv  9549  inf3lem6  9586  cantnflem1  9642  cardne  9918  cardsdomel  9927  carddom2  9930  cardmin2  9952  alephnbtwn  10024  infdif2  10162  fin4en1  10262  fin23lem31  10296  isf32lem5  10310  isf34lem4  10330  cfpwsdom  10537  fpwwe2  10596  addnidpi  10854  genpnnp  10958  btwnnz  12610  prime  12615  qsqueeze  13161  xralrple  13165  xmullem2  13225  xmulneg1  13229  ssfzoulel  13721  elfznelfzob  13734  bcval4  14272  seqcoll  14429  hashtpg  14450  swrd0  14623  fsumcvg  15678  fsumsplit  15707  fprodcvg  15896  fprodsplit  15932  dvdsle  16280  divalglem8  16370  bitsinv1lem  16411  2mulprm  16663  pockthg  16877  prmunb  16885  vdwlem6  16957  ramlb  16990  gsumzsplit  19857  obselocv  21637  opsrtoslem2  21963  psdmul  22053  elcls  22960  fbasrn  23771  ufilb  23793  ufilmax  23794  rnelfmlem  23839  alexsubALTlem4  23937  tsmssplit  24039  recld2  24703  logbgcd1irr  26704  fsumharmonic  26922  chtub  27123  lgsne0  27246  sltres  27574  nosupbnd2lem1  27627  nocvxminlem  27689  sltlpss  27819  sltmul2  28074  sltonold  28162  axlowdim  28888  wlkp1lem5  29605  wlkp1lem6  29606  cyclnspth  29731  eupth2lem3lem4  30160  cvnsym  32219  cvntr  32221  atcvati  32315  rmounid  32424  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemfrcn0  34521  ballotlemirc  34523  acycgr2v  35137  cusgracyclt3v  35143  fmlasucdisj  35386  nn0prpw  36311  onsucconni  36425  onint1  36437  icorempo  37339  relowlpssretop  37352  fvineqsneq  37400  lindsenlbs  37609  poimirlem16  37630  poimirlem26  37640  fdc  37739  lsatcvat  39043  hlrelat2  39397  ltltncvr  39417  islln2a  39511  islpln2a  39542  islvol2aN  39586  dvrelog2b  42054  mullt0b2d  42472  rencldnfilem  42808  cantnfresb  43313  dflim5  43318  ss2iundf  43648  uneqsn  44014  radcnvrat  44303  stoweidlem34  46032  oddneven  47645