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  2959  spcimegf  3529  spcegf  3531  spcimedv  3534  rspcimedv  3552  disjxun  5072  sotric  5531  sotrieq  5532  poirr2  6029  dfpo2  6199  funun  6480  imadif  6518  soisoi  7199  onnminsb  7649  oneqmin  7650  ordunisuc2  7691  limsssuc  7697  wfrlem10OLD  8149  tz7.48lem  8272  sdomdif  8912  sdomdomtrfi  8987  domsdomtrfi  8988  pssinf  9033  unblem1  9066  supnub  9221  infnlb  9251  elirrv  9355  inf3lem6  9391  cantnflem1  9447  cardne  9723  cardsdomel  9732  carddom2  9735  cardmin2  9757  alephnbtwn  9827  infdif2  9966  fin4en1  10065  fin23lem31  10099  isf32lem5  10113  isf34lem4  10133  cfpwsdom  10340  fpwwe2  10399  addnidpi  10657  genpnnp  10761  btwnnz  12396  prime  12401  qsqueeze  12935  xralrple  12939  xmullem2  12999  xmulneg1  13003  ssfzoulel  13481  elfznelfzob  13493  bcval4  14021  seqcoll  14178  hashtpg  14199  swrd0  14371  fsumcvg  15424  fsumsplit  15453  fprodcvg  15640  fprodsplit  15676  dvdsle  16019  divalglem8  16109  bitsinv1lem  16148  2mulprm  16398  pockthg  16607  prmunb  16615  vdwlem6  16687  ramlb  16720  gsumzsplit  19528  obselocv  20935  opsrtoslem2  21263  elcls  22224  fbasrn  23035  ufilb  23057  ufilmax  23058  rnelfmlem  23103  alexsubALTlem4  23201  tsmssplit  23303  recld2  23977  logbgcd1irr  25944  fsumharmonic  26161  chtub  26360  lgsne0  26483  axlowdim  27329  wlkp1lem5  28045  wlkp1lem6  28046  cyclnspth  28168  eupth2lem3lem4  28595  cvnsym  30652  cvntr  30654  atcvati  30748  rmounid  30843  ballotlemfc0  32459  ballotlemfcc  32460  ballotlemfrcn0  32496  ballotlemirc  32498  acycgr2v  33112  cusgracyclt3v  33118  fmlasucdisj  33361  sltres  33865  nosupbnd2lem1  33918  nocvxminlem  33972  sltlpss  34087  nn0prpw  34512  onsucconni  34626  onint1  34638  icorempo  35522  relowlpssretop  35535  fvineqsneq  35583  lindsenlbs  35772  poimirlem16  35793  poimirlem26  35803  fdc  35903  lsatcvat  37064  hlrelat2  37417  ltltncvr  37437  islln2a  37531  islpln2a  37562  islvol2aN  37606  dvrelog2b  40074  rencldnfilem  40642  ss2iundf  41267  uneqsn  41633  radcnvrat  41932  stoweidlem34  43575  oddneven  45096