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  2663  necon2bd  2949  spcimegf  3497  spcegf  3535  spcimedv  3538  rspcimedv  3556  disjxun  5084  exexneq  5380  sotric  5560  sotrieq  5561  poirr2  6079  dfpo2  6252  funun  6536  imadif  6574  soisoi  7274  onnminsb  7744  oneqmin  7745  ordunisuc2  7786  limsssuc  7792  tz7.48lem  8371  sdomdif  9054  sdomdomtrfi  9126  domsdomtrfi  9127  pssinf  9163  unblem1  9193  supnub  9366  infnlb  9397  elirrvOLD  9504  inf3lem6  9543  cantnflem1  9599  cardne  9878  cardsdomel  9887  carddom2  9890  cardmin2  9912  alephnbtwn  9982  infdif2  10120  fin4en1  10220  fin23lem31  10254  isf32lem5  10268  isf34lem4  10288  cfpwsdom  10496  fpwwe2  10555  addnidpi  10813  genpnnp  10917  btwnnz  12594  prime  12599  qsqueeze  13142  xralrple  13146  xmullem2  13206  xmulneg1  13210  ssfzoulel  13704  elfznelfzob  13718  bcval4  14258  seqcoll  14415  hashtpg  14436  swrd0  14610  fsumcvg  15663  fsumsplit  15692  fprodcvg  15884  fprodsplit  15920  dvdsle  16268  divalglem8  16358  bitsinv1lem  16399  2mulprm  16651  pockthg  16866  prmunb  16874  vdwlem6  16946  ramlb  16979  chnpof1  18585  gsumzsplit  19891  obselocv  21716  opsrtoslem2  22043  psdmul  22141  elcls  23047  fbasrn  23858  ufilb  23880  ufilmax  23881  rnelfmlem  23926  alexsubALTlem4  24024  tsmssplit  24126  recld2  24789  logbgcd1irr  26775  fsumharmonic  26993  chtub  27194  lgsne0  27317  ltsres  27645  nosupbnd2lem1  27698  nocvxminlem  27765  ltslpss  27919  ltmuls2  28182  ltonold  28272  axlowdim  29049  wlkp1lem5  29764  wlkp1lem6  29765  cyclnspth  29889  eupth2lem3lem4  30321  cvnsym  32381  cvntr  32383  atcvati  32477  rmounid  32584  ballotlemfc0  34658  ballotlemfcc  34659  ballotlemfrcn0  34695  ballotlemirc  34697  acycgr2v  35353  cusgracyclt3v  35359  fmlasucdisj  35602  nn0prpw  36526  onsucconni  36640  onint1  36652  icorempo  37678  relowlpssretop  37691  fvineqsneq  37739  lindsenlbs  37947  poimirlem16  37968  poimirlem26  37978  fdc  38077  lsatcvat  39507  hlrelat2  39860  ltltncvr  39880  islln2a  39974  islpln2a  40005  islvol2aN  40049  dvrelog2b  42516  mullt0b2d  42940  rencldnfilem  43263  cantnfresb  43767  dflim5  43772  ss2iundf  44101  uneqsn  44467  radcnvrat  44756  stoweidlem34  46477  oddneven  48117