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  2656  necon2bd  2942  spcimegf  3520  spcegf  3561  spcimedv  3564  rspcimedv  3582  disjxun  5107  exexneq  5396  sotric  5578  sotrieq  5579  poirr2  6099  dfpo2  6271  funun  6564  imadif  6602  soisoi  7305  onnminsb  7777  oneqmin  7778  ordunisuc2  7822  limsssuc  7828  tz7.48lem  8411  sdomdif  9094  sdomdomtrfi  9170  domsdomtrfi  9171  pssinf  9209  unblem1  9245  supnub  9419  infnlb  9450  elirrv  9555  inf3lem6  9592  cantnflem1  9648  cardne  9924  cardsdomel  9933  carddom2  9936  cardmin2  9958  alephnbtwn  10030  infdif2  10168  fin4en1  10268  fin23lem31  10302  isf32lem5  10316  isf34lem4  10336  cfpwsdom  10543  fpwwe2  10602  addnidpi  10860  genpnnp  10964  btwnnz  12616  prime  12621  qsqueeze  13167  xralrple  13171  xmullem2  13231  xmulneg1  13235  ssfzoulel  13727  elfznelfzob  13740  bcval4  14278  seqcoll  14435  hashtpg  14456  swrd0  14629  fsumcvg  15684  fsumsplit  15713  fprodcvg  15902  fprodsplit  15938  dvdsle  16286  divalglem8  16376  bitsinv1lem  16417  2mulprm  16669  pockthg  16883  prmunb  16891  vdwlem6  16963  ramlb  16996  gsumzsplit  19863  obselocv  21643  opsrtoslem2  21969  psdmul  22059  elcls  22966  fbasrn  23777  ufilb  23799  ufilmax  23800  rnelfmlem  23845  alexsubALTlem4  23943  tsmssplit  24045  recld2  24709  logbgcd1irr  26710  fsumharmonic  26928  chtub  27129  lgsne0  27252  sltres  27580  nosupbnd2lem1  27633  nocvxminlem  27695  sltlpss  27825  sltmul2  28080  sltonold  28168  axlowdim  28894  wlkp1lem5  29611  wlkp1lem6  29612  cyclnspth  29737  eupth2lem3lem4  30166  cvnsym  32225  cvntr  32227  atcvati  32321  rmounid  32430  ballotlemfc0  34490  ballotlemfcc  34491  ballotlemfrcn0  34527  ballotlemirc  34529  acycgr2v  35137  cusgracyclt3v  35143  fmlasucdisj  35386  nn0prpw  36306  onsucconni  36420  onint1  36432  icorempo  37334  relowlpssretop  37347  fvineqsneq  37395  lindsenlbs  37604  poimirlem16  37625  poimirlem26  37635  fdc  37734  lsatcvat  39038  hlrelat2  39392  ltltncvr  39412  islln2a  39506  islpln2a  39537  islvol2aN  39581  dvrelog2b  42049  mullt0b2d  42467  rencldnfilem  42801  cantnfresb  43306  dflim5  43311  ss2iundf  43641  uneqsn  44007  radcnvrat  44296  stoweidlem34  46025  oddneven  47635