Theorem con2d 136

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 132	. . 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  137  mt2d  138  pm3.2im  162  exists2  2747  necon2bd  3034  spcimegf  3591  spcegf  3593  spcimedv  3596  rspcimedv  3616  disjxun  5066  sotric  5503  sotrieq  5504  poirr2  5986  funun  6402  imadif  6440  soisoi  7083  onnminsb  7521  oneqmin  7522  ordunisuc2  7561  limsssuc  7567  wfrlem10  7966  tz7.48lem  8079  sdomdif  8667  pssinf  8730  unblem1  8772  supnub  8928  infnlb  8958  elirrv  9062  inf3lem6  9098  cantnflem1  9154  cardne  9396  cardsdomel  9405  carddom2  9408  cardmin2  9429  alephnbtwn  9499  infdif2  9634  fin4en1  9733  fin23lem31  9767  isf32lem5  9781  isf34lem4  9801  cfpwsdom  10008  fpwwe2  10067  addnidpi  10325  genpnnp  10429  btwnnz  12061  prime  12066  qsqueeze  12597  xralrple  12601  xmullem2  12661  xmulneg1  12665  ssfzoulel  13134  elfznelfzob  13146  bcval4  13670  seqcoll  13825  hashtpg  13846  swrd0  14022  fsumcvg  15071  fsumsplit  15099  fprodcvg  15286  fprodsplit  15322  dvdsle  15662  divalglem8  15753  bitsinv1lem  15792  2mulprm  16039  pockthg  16244  prmunb  16252  vdwlem6  16324  ramlb  16357  gsumzsplit  19049  opsrtoslem2  20267  obselocv  20874  elcls  21683  fbasrn  22494  ufilb  22516  ufilmax  22517  rnelfmlem  22562  alexsubALTlem4  22660  tsmssplit  22762  recld2  23424  logbgcd1irr  25374  fsumharmonic  25591  chtub  25790  lgsne0  25913  axlowdim  26749  wlkp1lem5  27461  wlkp1lem6  27462  cyclnspth  27583  eupth2lem3lem4  28012  cvnsym  30069  cvntr  30071  atcvati  30165  rmounid  30261  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemfrcn0  31789  ballotlemirc  31791  acycgr2v  32399  cusgracyclt3v  32405  fmlasucdisj  32648  dfpo2  32993  sltres  33171  nosupbnd2lem1  33217  nocvxminlem  33249  nn0prpw  33673  onsucconni  33787  onint1  33799  icorempo  34634  relowlpssretop  34647  fvineqsneq  34695  lindsenlbs  34889  poimirlem16  34910  poimirlem26  34920  fdc  35022  lsatcvat  36188  hlrelat2  36541  ltltncvr  36561  islln2a  36655  islpln2a  36686  islvol2aN  36730  rencldnfilem  39424  ss2iundf  40011  uneqsn  40380  radcnvrat  40653  stoweidlem34  42326  oddneven  43816