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  2686  necon2bd  2971  spcimegf  3514  spcegf  3546  spcimedv  3549  rspcimedv  3567  disjxun  5100  exexneq  5402  sotric  5588  sotrieq  5589  poirr2  6117  dfpo2  6299  funun  6586  imadif  6624  soisoi  7336  onnminsb  7813  oneqmin  7814  ordunisuc2  7855  limsssuc  7861  tz7.48lemOLD  8452  sdomdif  9145  sdomdomtrfi  9217  domsdomtrfi  9218  pssinf  9254  unblem1  9285  supnub  9455  infnlb  9486  elirrv  9592  elirrvOLDOLD  9594  inf3lem6  9635  cantnflem1  9691  cardne  10047  cardsdomel  10056  carddom2  10059  cardmin2  10081  alephnbtwn  10151  infdif2  10288  fin4en1  10388  fin23lem31  10422  isf32lem5  10436  isf34lem4  10456  cfpwsdom  10670  fpwwe2  10729  addnidpi  10987  genpnnp  11091  btwnnz  12776  prime  12781  qsqueeze  13332  xralrple  13336  xmullem2  13396  xmulneg1  13400  ssfzoulel  13896  elfznelfzob  13910  bcval4  14452  seqcoll  14610  hashtpg  14631  swrd0  14809  fsumcvg  15879  fsumsplit  15908  fprodcvg  16098  fprodsplit  16134  dvdsle  16481  divalglem8  16571  bitsinv1lem  16612  2mulprm  16869  pockthg  17085  prmunb  17093  vdwlem6  17165  ramlb  17198  chnpof1  18805  gsumzsplit  20142  obselocv  22035  lindsenlbs  22158  opsrtoslem2  22366  psdmul  22488  elcls  23392  fbasrn  24204  ufilb  24226  ufilmax  24227  rnelfmlem  24272  alexsubALTlem4  24370  tsmssplit  24472  recld2  25135  logbgcd1irr  27123  fsumharmonic  27340  chtub  27540  lgsne0  27663  ltsres  28020  nosupbnd2lem1  28073  nocvxminlem  28141  ltslpss  28295  ltmuls2  28558  ltonold  28648  axlowdim  29540  wlkp1lem5  30257  wlkp1lem6  30258  cyclnspth  30390  eupth2lem3lem4  30833  cvnsym  32893  cvntr  32895  atcvati  32989  rmounid  33134  ballotlemfc0  35168  ballotlemfcc  35169  ballotlemfrcn0  35205  ballotlemirc  35207  acycgr2v  35984  cusgracyclt3v  35990  fmlasucdisj  36233  nmulprop  37014  nn0prpw  37186  onsucconni  37300  onint1  37312  icorempo  38350  relowlpssretop  38363  fvineqsneq  38411  poimirlem16  38630  poimirlem26  38640  fdc  38755  lsatcvat  40183  hlrelat2  40536  ltltncvr  40556  islln2a  40650  islpln2a  40681  islvol2aN  40725  dvrelog2b  43192  mullt0b2d  43624  rencldnfilem  43903  cantnfresb  44402  dflim5  44407  ss2iundf  44735  uneqsn  45101  radcnvrat  45374  stoweidlem34  47120  oddneven  48818