Theorem con2d 135

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 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
4	3	con4d 116	1 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con2  136  mt2d  137  pm3.2im  161  exists2  2689  necon2bd  2975  spcimegf  3518  spcegf  3550  spcimedv  3553  rspcimedv  3571  disjxun  5104  exexneq  5407  sotric  5593  sotrieq  5594  poirr2  6130  dfpo2  6317  funun  6606  imadif  6646  soisoi  7359  onnminsb  7837  oneqmin  7838  ordunisuc2  7879  limsssuc  7885  tz7.48lemOLD  8479  sdomdif  9172  sdomdomtrfi  9244  domsdomtrfi  9245  pssinf  9281  unblem1  9312  supnub  9481  infnlb  9512  elirrv  9618  elirrvOLDOLD  9620  inf3lem6  9661  cantnflem1  9717  cardne  10073  cardsdomel  10082  carddom2  10085  cardmin2  10107  alephnbtwn  10177  infdif2  10314  fin4en1  10414  fin23lem31  10448  isf32lem5  10462  isf34lem4  10482  cfpwsdom  10696  fpwwe2  10755  addnidpi  11013  genpnnp  11117  btwnnz  12802  prime  12807  qsqueeze  13358  xralrple  13362  xmullem2  13422  xmulneg1  13426  ssfzoulel  13922  elfznelfzob  13936  bcval4  14478  seqcoll  14636  hashtpg  14657  swrd0  14836  fsumcvg  15907  fsumsplit  15936  fprodcvg  16126  fprodsplit  16162  dvdsle  16509  divalglem8  16599  bitsinv1lem  16640  2mulprm  16897  pockthg  17113  prmunb  17121  vdwlem6  17193  ramlb  17226  chnpof1  18833  gsumzsplit  20171  obselocv  22064  lindsenlbs  22187  opsrtoslem2  22395  psdmul  22517  elcls  23421  fbasrn  24233  ufilb  24255  ufilmax  24256  rnelfmlem  24301  alexsubALTlem4  24399  tsmssplit  24501  recld2  25164  logbgcd1irr  27152  fsumharmonic  27369  chtub  27569  lgsne0  27692  ltsres  28049  nosupbnd2lem1  28102  nocvxminlem  28170  ltslpss  28324  ltmuls2  28587  ltonold  28677  axlowdim  29569  wlkp1lem5  30286  wlkp1lem6  30287  cyclnspth  30419  eupth2lem3lem4  30862  cvnsym  32922  cvntr  32924  atcvati  33018  rmounid  33163  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemfrcn0  35232  ballotlemirc  35234  acycgr2v  36072  cusgracyclt3v  36078  fmlasucdisj  36331  nmulprop  37117  nn0prpw  37289  onsucconni  37403  onint1  37415  icorempo  38466  relowlpssretop  38479  fvineqsneq  38527  poimirlem16  38746  poimirlem26  38756  fdc  38871  lsatcvat  40299  hlrelat2  40652  ltltncvr  40672  islln2a  40766  islpln2a  40797  islvol2aN  40841  dvrelog2b  43308  mullt0b2d  43741  rencldnfilem  44020  cantnfresb  44518  dflim5  44523  ss2iundf  44851  uneqsn  45217  radcnvrat  45490  stoweidlem34  47249  oddneven  48947