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  3510  spcegf  3548  spcimedv  3551  rspcimedv  3569  disjxun  5098  exexneq  5391  sotric  5570  sotrieq  5571  poirr2  6089  dfpo2  6262  funun  6546  imadif  6584  soisoi  7284  onnminsb  7754  oneqmin  7755  ordunisuc2  7796  limsssuc  7802  tz7.48lem  8382  sdomdif  9065  sdomdomtrfi  9137  domsdomtrfi  9138  pssinf  9174  unblem1  9204  supnub  9377  infnlb  9408  elirrvOLD  9515  inf3lem6  9554  cantnflem1  9610  cardne  9889  cardsdomel  9898  carddom2  9901  cardmin2  9923  alephnbtwn  9993  infdif2  10131  fin4en1  10231  fin23lem31  10265  isf32lem5  10279  isf34lem4  10299  cfpwsdom  10507  fpwwe2  10566  addnidpi  10824  genpnnp  10928  btwnnz  12580  prime  12585  qsqueeze  13128  xralrple  13132  xmullem2  13192  xmulneg1  13196  ssfzoulel  13688  elfznelfzob  13702  bcval4  14242  seqcoll  14399  hashtpg  14420  swrd0  14594  fsumcvg  15647  fsumsplit  15676  fprodcvg  15865  fprodsplit  15901  dvdsle  16249  divalglem8  16339  bitsinv1lem  16380  2mulprm  16632  pockthg  16846  prmunb  16854  vdwlem6  16926  ramlb  16959  chnpof1  18565  gsumzsplit  19868  obselocv  21695  opsrtoslem2  22023  psdmul  22121  elcls  23029  fbasrn  23840  ufilb  23862  ufilmax  23863  rnelfmlem  23908  alexsubALTlem4  24006  tsmssplit  24108  recld2  24771  logbgcd1irr  26772  fsumharmonic  26990  chtub  27191  lgsne0  27314  ltsres  27642  nosupbnd2lem1  27695  nocvxminlem  27762  ltslpss  27916  ltmuls2  28179  ltonold  28269  axlowdim  29046  wlkp1lem5  29761  wlkp1lem6  29762  cyclnspth  29886  eupth2lem3lem4  30318  cvnsym  32377  cvntr  32379  atcvati  32473  rmounid  32580  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemfrcn0  34707  ballotlemirc  34709  acycgr2v  35363  cusgracyclt3v  35369  fmlasucdisj  35612  nn0prpw  36536  onsucconni  36650  onint1  36662  icorempo  37595  relowlpssretop  37608  fvineqsneq  37656  lindsenlbs  37855  poimirlem16  37876  poimirlem26  37886  fdc  37985  lsatcvat  39415  hlrelat2  39768  ltltncvr  39788  islln2a  39882  islpln2a  39913  islvol2aN  39957  dvrelog2b  42425  mullt0b2d  42843  rencldnfilem  43166  cantnfresb  43670  dflim5  43675  ss2iundf  44004  uneqsn  44370  radcnvrat  44659  stoweidlem34  46381  oddneven  47993