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  2661  necon2bd  2955  spcimegf  3550  spcegf  3591  spcimedv  3594  rspcimedv  3612  disjxun  5140  exexneq  5438  sotric  5621  sotrieq  5622  poirr2  6143  dfpo2  6315  funun  6611  imadif  6649  soisoi  7349  onnminsb  7820  oneqmin  7821  ordunisuc2  7866  limsssuc  7872  wfrlem10OLD  8359  tz7.48lem  8482  sdomdif  9166  sdomdomtrfi  9242  domsdomtrfi  9243  pssinf  9293  unblem1  9329  supnub  9503  infnlb  9533  elirrv  9637  inf3lem6  9674  cantnflem1  9730  cardne  10006  cardsdomel  10015  carddom2  10018  cardmin2  10040  alephnbtwn  10112  infdif2  10250  fin4en1  10350  fin23lem31  10384  isf32lem5  10398  isf34lem4  10418  cfpwsdom  10625  fpwwe2  10684  addnidpi  10942  genpnnp  11046  btwnnz  12696  prime  12701  qsqueeze  13244  xralrple  13248  xmullem2  13308  xmulneg1  13312  ssfzoulel  13800  elfznelfzob  13813  bcval4  14347  seqcoll  14504  hashtpg  14525  swrd0  14697  fsumcvg  15749  fsumsplit  15778  fprodcvg  15967  fprodsplit  16003  dvdsle  16348  divalglem8  16438  bitsinv1lem  16479  2mulprm  16731  pockthg  16945  prmunb  16953  vdwlem6  17025  ramlb  17058  gsumzsplit  19946  obselocv  21749  opsrtoslem2  22081  psdmul  22171  elcls  23082  fbasrn  23893  ufilb  23915  ufilmax  23916  rnelfmlem  23961  alexsubALTlem4  24059  tsmssplit  24161  recld2  24837  logbgcd1irr  26838  fsumharmonic  27056  chtub  27257  lgsne0  27380  sltres  27708  nosupbnd2lem1  27761  nocvxminlem  27823  sltlpss  27946  sltmul2  28198  sltonold  28284  axlowdim  28977  wlkp1lem5  29696  wlkp1lem6  29697  cyclnspth  29822  eupth2lem3lem4  30251  cvnsym  32310  cvntr  32312  atcvati  32406  rmounid  32515  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemfrcn0  34533  ballotlemirc  34535  acycgr2v  35156  cusgracyclt3v  35162  fmlasucdisj  35405  nn0prpw  36325  onsucconni  36439  onint1  36451  icorempo  37353  relowlpssretop  37366  fvineqsneq  37414  lindsenlbs  37623  poimirlem16  37644  poimirlem26  37654  fdc  37753  lsatcvat  39052  hlrelat2  39406  ltltncvr  39426  islln2a  39520  islpln2a  39551  islvol2aN  39595  dvrelog2b  42068  rencldnfilem  42836  cantnfresb  43342  dflim5  43347  ss2iundf  43677  uneqsn  44043  radcnvrat  44338  stoweidlem34  46054  oddneven  47636